Ignore:
Timestamp:
Feb 22, 2011, 4:23:13 PM (9 years ago)
Author:
campbell
Message:

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Mem.ma

    r500 r583  
    644644  given offset falls within the bounds of the corresponding block. *)
    645645
    646 definition valid_pointer : mem → region → block → Z → bool ≝
     646definition valid_pointer : mem → region → block → offset → bool ≝
    647647λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    648   Zleb (low_bound m b) ofs
    649   Zltb ofs (high_bound m b) ∧
     648  Zleb (low_bound m b) (offv ofs)
     649  Zltb (offv ofs) (high_bound m b) ∧
    650650  is_pointer_compat b r.
    651651
     
    680680let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    681681  match addr with
    682   [ Vptr r b p ofs ⇒ load chunk m r b (signed ofs)
     682  [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs)
    683683  | _ ⇒ None ? ].
    684684
     
    727727λchunk,m,addr,v.
    728728  match addr with
    729   [ Vptr r b p ofs ⇒ store chunk m r b (signed ofs) v
     729  [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v
    730730  | _ ⇒ None ? ].
    731731
Note: See TracChangeset for help on using the changeset viewer.