Changeset 2395 for src/Clight/Csem.ma


Ignore:
Timestamp:
Oct 12, 2012, 3:33:53 PM (8 years ago)
Author:
campbell
Message:

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2391 r2395  
    348348        match v2 with
    349349        [ Vptr ptr2 ⇒
    350           if valid_pointer m ptr1
    351           ∧ valid_pointer m ptr2 then
    352             if eq_block (pblock ptr1) (pblock ptr2)
     350          (* Pointers one-off-the-end require careful treatment - they may end
     351             up equal to a pointer to another object.  I don't think we have
     352             the corresponding definitions in the back-end, so we may need to
     353             compromise on this; if so, the pointer comparison in FrontEndOps
     354             will need changed too. *)
     355          if eq_block (pblock ptr1) (pblock ptr2) then
     356            if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧
     357               (valid_pointer m ptr2 ∨ end_pointer m ptr2)
    353358            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    354             else sem_cmp_mismatch c
    355           else None ?
     359            else None ?
     360          else
     361            if valid_pointer m ptr1 ∧
     362               valid_pointer m ptr2
     363            then sem_cmp_mismatch c
     364            else None ?
    356365        | Vnull ⇒ sem_cmp_mismatch c
    357366        | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.