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

    r478 r480  
    406406| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
    407407
    408 ninductive type_space : type → memory_space → Prop ≝
     408ninductive type_space : type → region → Prop ≝
    409409| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    410410| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    470470  reference, the pointer [Vptr b ofs] is returned. *)
    471471
    472 nlet rec load_value_of_type (ty: type) (m: mem) (psp:memory_space) (b: block) (ofs: int) : option val ≝
     472nlet rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
    473473  match access_mode ty with
    474474  [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
     
    482482  This is allowed only if [ty] indicates an access by value. *)
    483483
    484 nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:memory_space) (loc: block) (ofs: int) (v: val) : option mem ≝
     484nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
    485485  match access_mode ty_dest with
    486486  [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
     
    633633  that contains the value of the expression [a]. *)
    634634
    635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝
     635with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
    636636  | eval_Evar_local:   ∀id,l,ty.
    637637      (* XXX notation? e!id*) get ??? id e = Some ? l →
     
    699699  (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. P a psp l ofs tr H1 → P ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    700700  (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. P a psp l ofs tr H1 → P ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    701   (a:expr) (psp:memory_space) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
     701  (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
    702702  match ev with
    703703  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    717717    ∀x3: mem.
    718718     ∀x4: expr.
    719       ∀x5: memory_space.
     719      ∀x5: region.
    720720       ∀x6: block.
    721721        ∀x7: int.
     
    723723          ∀P:
    724724            ∀_z1430: expr.
    725              ∀_z1429: memory_space.
     725             ∀_z1429: region.
    726726              ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.
    727727           ∀_H1: ?.
     
    737737      (λx3:mem.
    738738        (λx4:expr.
    739           (λx5:memory_space.
     739          (λx5:region.
    740740            (λx6:block.
    741741              (λx7:int.
    742742                (λx8:trace.
    743743                  (λP:∀_z1430: expr.
    744                         ∀_z1429: memory_space.
     744                        ∀_z1429: region.
    745745                         ∀_z1428: block.
    746746                          ∀_z1427: int. ∀_z1426: trace. Prop.
     
    752752                              (λHterm:eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
    753753                                ((λHcut:∀z1435: eq expr x4 x4.
    754                                           ∀z1434: eq memory_space x5 x5.
     754                                          ∀z1434: eq region x5 x5.
    755755                                           ∀z1433: eq block x6 x6.
    756756                                            ∀z1432: eq int x7 x7.
     
    758758                                              P x4 x5 x6 x7 x8.
    759759                                   (Hcut (refl expr x4)
    760                                      (refl memory_space x5) (refl block x6)
     760                                     (refl region x5) (refl block x6)
    761761                                     (refl int x7) (refl trace x8)))
    762762                                  ?)))))))))))))))).
     
    831831  (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    832832  (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    833   (a:expr) (psp:memory_space) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
     833  (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
    834834  match ev with
    835835  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
     
    886886  | Kswitch: cont -> cont
    887887       (**r catches [break] statements arising out of [switch] *)
    888   | Kcall: option (memory_space × block × int × type) ->   (**r where to store result *)
     888  | Kcall: option (region × block × int × type) ->   (**r where to store result *)
    889889           function ->                      (**r calling function *)
    890890           env ->                           (**r local env of calling function *)
Note: See TracChangeset for help on using the changeset viewer.