- Timestamp:
- Jun 10, 2011, 3:10:27 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r931 r932 1953 1953 >ignore_clock 1954 1954 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG] 1955 [1,2,3,4: XXX 1956 >get_arg_8_set_program_counter try % [2:%] 1957 >get_arg_8_set_program_counter [2:%] 1958 >get_arg_8_set_program_counter [2:%] 1959 >get_arg_8_set_code_memory 1960 >get_arg_8_set_program_counter [2,4:%] 1961 >get_arg_8_set_program_counter [2,4:%] 1962 >get_arg_8_set_code_memory 1963 cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags 1964 *)#EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; % 1955 [1,2,3,4: cases (half_add ???) #carry #result 1956 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; 1957 whd in ⊢ (??%%) 1958 % 1965 1959 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1966 1960
Note: See TracChangeset
for help on using the changeset viewer.