- Timestamp:
- Jun 10, 2011, 3:20:34 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r932 r933 1930 1930 whd in ⊢ (???% → ??%?); 1931 1931 >ignore_clock 1932 >get_arg_8_set_program_counter [2,4,6:%] 1933 >get_arg_8_set_program_counter [2,4,6:%] 1934 >get_arg_8_set_program_counter [2,4,6:%] 1935 >get_arg_8_set_program_counter [2,4,6:%] 1936 >get_arg_8_set_code_memory 1937 >get_arg_8_set_program_counter [2,4,6:%] 1938 >get_arg_8_set_program_counter [2,4,6:%] 1939 >get_arg_8_set_code_memory 1940 [1,2: cases (add_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?) 1941 | cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?)] 1932 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; 1933 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2 1934 normalize nodelta; 1935 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 1942 1936 #result #flags 1943 1937 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; 1944 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1938 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1945 1939 | (* INC *) #arg1 #H1 #H2 #EQ %[@1] 1946 1940 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) … … 1955 1949 [1,2,3,4: cases (half_add ???) #carry #result 1956 1950 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; 1957 whd in ⊢ (??%%) 1958 % 1951 XXX 1959 1952 >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags % 1960 1953
Note: See TracChangeset
for help on using the changeset viewer.