Changeset 2185 for src/common/GenMem.ma


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

    r2180 r2185  
    178178//; qed.
    179179
     180(* XXX note that this won't allow access to negative offsets, and we don't
     181   currently provide any other means to access them.  We could choose to get
     182   rid of them entirely. *)
    180183
    181184(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
     
    186189  if Zltb (block_id b) (nextblock … m) then
    187190   let content ≝ blocks … m b in
    188    let off ≝ offv (poff ptr) in
     191   let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
    189192   if andb (Zleb (low … content) off) (Zltb off (high … content)) then
    190193    Some … (F b content off)
Note: See TracChangeset for help on using the changeset viewer.