Ignore:
Timestamp:
Apr 3, 2013, 3:01:54 PM (6 years ago)
Author:
tranquil
Message:

fixed change of Mov

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r3039 r3078  
    661661              try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
    662662          |2,3,5: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
    663           |7: * [ #x normalize nodelta #y #z #_ #_ % ]
    664             * #x @(subaddressing_mode_elim … x) [2,3: #y] * #lbl #off
    665             normalize nodelta #_ #_ lapply (vsplit ? 8 8 ?) * #w1 #w2 % ]
     663          |7: *
     664            [ #x @(subaddressing_mode_elim … x)
     665            | * #x  @(subaddressing_mode_elim … x) [2,3: #y] *
     666            ] normalize nodelta #lbl #off #_ #_
     667            @pair_elim * #addr normalize nodelta #_ %
     668          ]
    666669            #id lapply (Hpc_equal i (le_S_to_le … Hi))
    667670            lapply (Hpc_equal (S i) Hi)
Note: See TracChangeset for help on using the changeset viewer.