Changeset 2429


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.

Location:
src
Files:
2 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 ?
  • src/common/FrontEndMem.ma

    r2395 r2429  
    6161   the result when coalescing blocks. *)
    6262
     63(* Reverting to CompCert restriction.
    6364definition end_pointer : mem → pointer → bool ≝
    6465λm,ptr.
    6566  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
    6667  eqZb off (high_bound m (pblock ptr)).
     68*)
    6769
    68 
Note: See TracChangeset for help on using the changeset viewer.