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

    r500 r583  
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc ofs)
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs))
    419419        | inr _ ⇒ None ?
    420420        ]
     
    523523  init_mem_
    524524  (λF,ge. functions ? ge) (* find_funct_ptr *)
    525   (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     525  (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    526526  (λF,ge. symbols ? ge) (* find_symbol *)
    527527(*  ?
Note: See TracChangeset for help on using the changeset viewer.