Ignore:
Timestamp:
Jul 13, 2012, 7:59:43 PM (8 years ago)
Author:
campbell
Message:

Use bitvectors for offsets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndMem.ma

    r1993 r2185  
    5050
    5151definition valid_pointer : mem → pointer → bool ≝
    52 λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
    53   Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
    54   Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
     52λm,ptr.
     53  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
     54  Zltb (block_id (pblock ptr)) (nextblock m) ∧
     55  Zleb (low_bound m (pblock ptr)) off ∧
     56  Zleb off (high_bound m (pblock ptr)).
    5557
Note: See TracChangeset for help on using the changeset viewer.