Changeset 1978


Ignore:
Timestamp:
May 22, 2012, 12:37:28 AM (6 years ago)
Author:
sacerdot
Message:

Two more cases completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1977 r1978  
    678678  cases daemon
    679679  (* 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  *)
    681681  (* XXX: simplify the right hand side *)
    682682  >p normalize nodelta
     
    698698  (* XXX: simplify the left hand side *)
    699699  @(pair_replace ?????????? p)
    700   [1,3,5,7,9,11,13,15:
     700  [1,3,5,7,9,11,13,15,17:
    701701    cases daemon
    702   |12,14,16:
     702  |14,16,18:
    703703    normalize nodelta
    704704    @(pair_replace ?????????? p1)
     
    814814    cases daemon
    815815  ]
    816 |33,34,35: (* ANL, ORL, XRL *)
     816|33,34,35,48: (* ANL, ORL, XRL, MOVX *)
    817817  (* 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
    823821  ]
    824822  @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta
     
    845843  (* XXX: work on both sides *)
    846844  cases daemon
    847 |
     845|47: (* MOV *)
     846|* (* JUMPS!!! *)
     847]
    848848qed.
    849849(*   
Note: See TracChangeset for help on using the changeset viewer.