Ignore:
Timestamp:
Jul 31, 2012, 6:08:00 PM (8 years ago)
Author:
sacerdot
Message:

PUSH case almost finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2279 r2282  
    863863                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
    864864             else
    865                match lookup_from_internal_ram … d M with
    866                [ None ⇒
    867                    Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
    868                | Some ul_addr ⇒
    869                    Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M)
    870                ]
     865               Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (lookup_from_internal_ram … d M) M)
    871866         | _ ⇒ λother: False. ⊥
    872867         ] (subaddressing_modein … addr1)
Note: See TracChangeset for help on using the changeset viewer.