Changeset 2429 for src/Clight


Ignore:
Timestamp:
Nov 6, 2012, 12:53:46 PM (7 years ago)
Author:
garnier
Message:

Restrict semantics of pointer comparison to what CompCert? does - i.e. no more pointer one of the end of a block.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2428 r2429  
    354354             will need changed too. *)
    355355          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)
     356            if (valid_pointer m ptr1 ∧ valid_pointer m ptr2)
    358357            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    359358            else None ?
Note: See TracChangeset for help on using the changeset viewer.