Changeset 2429 for src/common


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/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.