Changeset 2433


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

Tidy up Clight pointer comparison.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2429 r2433  
    348348        match v2 with
    349349        [ Vptr 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 ∧ valid_pointer m ptr2)
     350          if (valid_pointer m ptr1 ∧ valid_pointer m ptr2)
     351          then
     352            if eq_block (pblock ptr1) (pblock ptr2)
    357353            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    358             else None ?
    359           else
    360             if valid_pointer m ptr1 ∧
    361                valid_pointer m ptr2
    362             then sem_cmp_mismatch c
    363             else None ?
     354            else sem_cmp_mismatch c
     355          else None ?
    364356        | Vnull ⇒ sem_cmp_mismatch c
    365357        | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.