Changeset 1540 for src/ASM/Interpret.ma
- Timestamp:
- Nov 23, 2011, 4:03:38 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1538 r1540 589 589 let s ≝ add_ticks2 s in 590 590 s 591 ]. (*14s*) 591 ]. cases daemon (* 592 (*14s*) 592 593 (* try assumption (*20s*) 593 594 try % (*6s*) … … 606 607 normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock 607 608 >set_8051_sfr_ignores_clock >clock_set_clock // 608 |2 4:609 |21,24: 609 610 normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock 610 611 >clock_set_clock // 611 |25: normalize nodelta @(le_n (clock M s)) 612 |25,26,28: 613 normalize nodelta // 614 |30,32,35: 615 normalize nodelta // 612 616 |13,14,15,16,18: 613 617 normalize nodelta >set_arg_8_ignores_clock >clock_set_clock // 614 618 |17: 615 619 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: 620 |3,4,7,8,11,12,19,20,33,36: cases daemon 621 |27,29,31,34,37: 622 normalize nodelta >set_program_counter_ignores_clock >clock_set_clock // 623 |22: 624 normalize nodelta <set_flags_ignores_clock >clock_set_clock // 618 625 [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock 619 626 >clock_set_clock // *) (* segfault now *) … … 640 647 |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*) 641 648 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *) 642 |*:cases daemon] 643 qed. 644 645 (*CSC: indexing diverges, why?*) 646 example set_program_counter_ignores_clock: 647 ∀M.∀s: PreStatus M. 648 ∀pc: Word. 649 clock … (set_program_counter … s pc) = clock … s. 650 // 651 qed. 652 653 lemma set_8051_sfr_ignores_clock: 654 ∀M.∀s: PreStatus M. 655 ∀sfr: SFR8051. 656 ∀v: Byte. 657 clock … (set_8051_sfr ? s sfr v) = clock … s. 658 // 649 |*:cases daemon] *) 659 650 qed. 660 651
Note: See TracChangeset
for help on using the changeset viewer.