Changeset 2258 for src/ASM/Test.ma
- Timestamp:
- Jul 25, 2012, 1:47:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2247 r2258 982 982 ∀cm. 983 983 ∀ps. 984 ∀addr : [[dptr]].985 ∀v : Word.984 ∀addr,addr': [[dptr]]. 985 ∀v,v': Word. 986 986 ∀M. ∀sigma. ∀policy. ∀s'. 987 987 status_of_pseudo_status M cm ps sigma policy = s' → 988 v=v' → addr=addr' → 988 989 set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 989 s' v addr=990 s' v' addr' = 990 991 status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. 991 #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl 992 #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl 993 <addr_refl #v_refl <v_refl 992 994 @(subaddressing_mode_elim … addr) 993 995 whd in match set_arg_16; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.