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/common/FrontEndMem.ma

    r2185 r2395  
    4646  | _ ⇒ None ? ].
    4747
    48 (* Only used by Clight semantics for pointer comparisons.  So in contrast to
    49    CompCert, we allow a pointer-to-one-off-the-end. *)
     48(* A pointer that can be dereferenced.  Only used for front-end pointer
     49   comparison at present. *)
    5050
    5151definition valid_pointer : mem → pointer → bool ≝
     
    5454  Zltb (block_id (pblock ptr)) (nextblock m) ∧
    5555  Zleb (low_bound m (pblock ptr)) off ∧
    56   Zleb off (high_bound m (pblock ptr)).
     56  Zltb off (high_bound m (pblock ptr)).
    5757
     58(* In contrast to CompCert, we also allow a pointer-to-one-off-the-end.  This is
     59   not entirely straightforward, as comparisons of an off-the-end pointer with a
     60   pointer from another block cannot be defined; if we did then we might change
     61   the result when coalescing blocks. *)
     62
     63definition end_pointer : mem → pointer → bool ≝
     64λm,ptr.
     65  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
     66  eqZb off (high_bound m (pblock ptr)).
     67
     68
Note: See TracChangeset for help on using the changeset viewer.