Changeset 1538 for src/ASM


Ignore:
Timestamp:
Nov 23, 2011, 12:28:51 PM (8 years ago)
Author:
mulligan
Message:

changes to execute_1_0 proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1534 r1538  
    431431            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
    432432            let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in
    433               set_arg_8 ? s addr2 old_acc
     433              eject … (set_arg_8 ? s addr2 old_acc)
    434434        | XCHD addr1 addr2 ⇒
    435435            let s ≝ add_ticks1 s in
     
    440440            let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in
    441441              set_arg_8 ? s addr2 new_arg
    442         | _ ⇒ ?
    443         ].
    444442        | RET ⇒
    445443            let s ≝ add_ticks1 s in
     
    598596      @ I
    599597    ) (*34s*) *)
    600  [9: normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
    601      >clock_set_clock //
     598 try assumption
     599 try @le_n
     600 [2,6,10: normalize @I
     601 |1,5: /by/ (* 81 seconds *)
     602 |9:
     603   normalize nodelta <set_flags_ignores_clock >set_arg_8_ignores_clock
     604   >clock_set_clock //
     605 |23:
     606   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
     607   >set_8051_sfr_ignores_clock >clock_set_clock //
     608 |24:
     609   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
     610   >clock_set_clock //
     611 |25: normalize nodelta @(le_n (clock M s))
     612 |13,14,15,16,18:
     613   normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
     614 |17:
     615   normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock //
     616 |17,18,23,24,25,28: /by/
     617 |3,4,7,8,11,12,19,20:
     618 [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
     619     >clock_set_clock // *) (* segfault now *)
    602620 |32,34: cases l #either normalize nodelta cases either
    603621      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
Note: See TracChangeset for help on using the changeset viewer.