Changeset 2257 for src/ASM


Ignore:
Timestamp:
Jul 25, 2012, 1:13:52 PM (7 years ago)
Author:
mulligan
Message:

Daemon in SETB case closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2256 r2257  
    21402140      ]
    21412141    ]
    2142   |*)44: (* MOVX *)
     2142  |44: (* MOVX *)
    21432143    >EQP -P normalize nodelta
    21442144    inversion addr
     
    22132213      ]
    22142214    ]
    2215   |45: (* SETB *)
     2215  |*)45: (* SETB *)
     2216    >EQs >EQticks <instr_refl
    22162217    >EQP -P normalize nodelta
    22172218    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     
    22232224    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    22242225    change with (set_arg_1 ????? = ?)
    2225     >EQs >EQticks <instr_refl
    22262226    @set_arg_1_status_of_pseudo_status try %
    2227     lapply addressing_mode_ok_assm_1 (* XXX: move into a lemma *)
    2228     @(subaddressing_mode_elim … b)
    2229     [1,3:
    2230       #_ @I
    2231     |2,4:
    2232       #w cases daemon
    2233       (* XXX: need changes to addressing_mode_ok *)
     2227    [1:
     2228      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
     2229    |2:
     2230      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    22342231    ]
    22352232  |46: (* PUSH *)
Note: See TracChangeset for help on using the changeset viewer.