Changeset 1978
 Timestamp:
 May 22, 2012, 12:37:28 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1977 r1978 678 678 cases daemon 679 679 (* XXX: work on both sides *) 680 1,2,3,9, 51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI *)680 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *) 681 681 (* XXX: simplify the right hand side *) 682 682 >p normalize nodelta … … 698 698 (* XXX: simplify the left hand side *) 699 699 @(pair_replace ?????????? p) 700 [1,3,5,7,9,11,13,15 :700 [1,3,5,7,9,11,13,15,17: 701 701 cases daemon 702 1 2,14,16:702 14,16,18: 703 703 normalize nodelta 704 704 @(pair_replace ?????????? p1) … … 814 814 cases daemon 815 815 ] 816 33,34,35 : (* ANL, ORL, XRL*)816 33,34,35,48: (* ANL, ORL, XRL, MOVX *) 817 817 (* XXX: simplify the right hand side *) 818 [1,2,3: 819 inversion addr #addr' #EQaddr normalize nodelta 820 [1,3: 821 inversion addr' #addr'' #EQaddr' normalize nodelta 822 ] 818 inversion addr #addr' #EQaddr normalize nodelta 819 [1,3: 820 inversion addr' #addr'' #EQaddr' normalize nodelta 823 821 ] 824 822 @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta … … 845 843 (* XXX: work on both sides *) 846 844 cases daemon 847  845 47: (* MOV *) 846 * (* JUMPS!!! *) 847 ] 848 848 qed. 849 849 (*
Note: See TracChangeset
for help on using the changeset viewer.