Changeset 2038


Ignore:
Timestamp:
Jun 8, 2012, 6:17:02 PM (5 years ago)
Author:
sacerdot
Message:

split => vsplit

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2034 r2038  
    126126                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    127127                        #result #flags normalize nodelta
    128                         cases (split bool 8 8 result)
     128                        cases (vsplit bool 8 8 result)
    129129                        #upper #lower normalize nodelta
    130130                        cases (eq_bv 8 upper (zero 8))
     
    135135                      |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
    136136                        normalize nodelta
    137                         cases (split bool 5 11 ?) #addr1 #addr2
    138                         cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
     137                        cases (vsplit bool 5 11 ?) #addr1 #addr2
     138                        cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    139139                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    140140                        #result #flags normalize nodelta
    141                         cases (split bool 8 8 result)
     141                        cases (vsplit bool 8 8 result)
    142142                        #upper #lower normalize nodelta
    143143                        #H >(not_true_is_false ? (proj2 ?? (proj1 ?? H)))
     
    145145                      |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
    146146                        normalize nodelta
    147                         cases (split bool 5 11 ?) #addr1 #addr2
    148                         cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
     147                        cases (vsplit bool 5 11 ?) #addr1 #addr2
     148                        cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    149149                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    150150                        #result #flags normalize nodelta
    151                         cases (split bool 8 8 result)
     151                        cases (vsplit bool 8 8 result)
    152152                        #upper #lower normalize nodelta
    153153                        #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
     
    172172                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    173173                          #result #flags normalize nodelta
    174                           cases (split bool 8 8 result)
     174                          cases (vsplit bool 8 8 result)
    175175                          #upper #lower normalize nodelta
    176176                          cases (eq_bv 8 upper (zero 8))
     
    214214                          whd in match short_jump_cond; whd in match medium_jump_cond;
    215215                          normalize nodelta
    216                           cases (split bool 5 11 ?) #addr1 #addr2
    217                           cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
     216                          cases (vsplit bool 5 11 ?) #addr1 #addr2
     217                          cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    218218                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    219219                          #result #flags normalize nodelta
    220                           cases (split bool 8 8 result)
     220                          cases (vsplit bool 8 8 result)
    221221                          #upper #lower normalize nodelta
    222222                          #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
     
    224224                          whd in match short_jump_cond; whd in match medium_jump_cond;
    225225                          normalize nodelta
    226                           cases (split bool 5 11 ?) #addr1 #addr2
    227                           cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
     226                          cases (vsplit bool 5 11 ?) #addr1 #addr2
     227                          cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
    228228                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
    229229                          #result #flags normalize nodelta
    230                           cases (split bool 8 8 result)
     230                          cases (vsplit bool 8 8 result)
    231231                          #upper #lower normalize nodelta
    232232                          #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
Note: See TracChangeset for help on using the changeset viewer.