Changeset 2432


Ignore:
Timestamp:
Nov 6, 2012, 3:17:23 PM (7 years ago)
Author:
campbell
Message:

Remove off-the-end pointers from front end ops.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r2395 r2432  
    409409  [ Vptr ptr1 ⇒ match v2 with
    410410    [ Vptr ptr2 ⇒
    411         if eq_block (pblock ptr1) (pblock ptr2) then
    412           if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧
    413              (valid_pointer m ptr2 ∨ end_pointer m ptr2)
     411        if valid_pointer m ptr1 ∧ valid_pointer m ptr2
     412        then
     413          if eq_block (pblock ptr1) (pblock ptr2)
    414414          then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    415           else None ?
    416         else
    417           if valid_pointer m ptr1 ∧
    418              valid_pointer m ptr2
    419           then ev_cmp_mismatch c
    420           else None ?
     415          else ev_cmp_mismatch c
     416        else None ?
    421417    | Vnull  ⇒ ev_cmp_mismatch c
    422418    | _ ⇒ None ? ]
     
    509505  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
    510506| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
    511   whd in ⊢ (??%? → ?); [ cases (andb ??) cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
     507  whd in ⊢ (??%? → ?); [ cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
    512508] qed.
    513509
Note: See TracChangeset for help on using the changeset viewer.