Ignore:
Timestamp:
Jan 25, 2011, 5:30:37 PM (9 years ago)
Author:
campbell
Message:

"memory_space" to "region" replacement to match ocaml code

File:
1 edited

Legend:

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

    r474 r480  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*;
     68  find_symbol: ∀F: Type. genv_t F → ident → option (region × block)(*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
     
    317317  functions: block → option F;
    318318  nextfunction: Z;
    319   symbols: ident → option (memory_space × block)
     319  symbols: ident → option (region × block)
    320320}.
    321321(*
     
    346346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
    347347
    348 ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝
     348ndefinition add_symbol : ∀F:Type. ident → region → block → genv F → genv F ≝
    349349λF,name,bsp,b,g.
    350350  mk_genv F (functions ? g)
     
    397397
    398398ndefinition add_globals : ∀F,V:Type.
    399        genv F × mem → list (ident × (list init_data) × memory_space × V) →
     399       genv F × mem → list (ident × (list init_data) × region × V) →
    400400       genv F × mem ≝
    401401λF,V,init,vars.
    402402  foldr ??
    403     (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem.
     403    (λid_init: ident × (list init_data) × region × V. λg_st: genv F × mem.
    404404      match id_init with [ mk_pair id_init1 info ⇒
    405405      match id_init1 with [ mk_pair id_init2 bsp ⇒
Note: See TracChangeset for help on using the changeset viewer.