Changeset 932


Ignore:
Timestamp:
Jun 10, 2011, 3:10:27 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r931 r932  
    19531953       >ignore_clock
    19541954       @(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         %
    19651959       >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %
    19661960 
Note: See TracChangeset for help on using the changeset viewer.