Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (9 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

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

    r498 r500  
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
    415415      [ None ⇒ None ?
    416       | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' b' ofs)
     416      | Some b' ⇒
     417        match pointer_compat_dec b' r' with
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc ofs)
     419        | inr _ ⇒ None ?
     420        ]
    417421      ]
    418422  | Init_space n ⇒ Some ? m
     
    519523  init_mem_
    520524  (λF,ge. functions ? ge) (* find_funct_ptr *)
    521   (λ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 o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    522526  (λF,ge. symbols ? ge) (* find_symbol *)
    523527(*  ?
Note: See TracChangeset for help on using the changeset viewer.