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

    r478 r480  
    162162].
    163163
    164 ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
     164ndefinition ms_eq_dec : ∀s1,s2:region. (s1 = s2) + (s1 ≠ s2).
    165165#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    166166
     
    277277  ]
    278278]
    279 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (memory_space × block × int × trace) ≝
     279and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (region × block × int × trace) ≝
    280280  match e' with
    281281  [ Evar id ⇒
     
    303303  | _ ⇒ Error ?
    304304  ]
    305 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (memory_space × block × int × trace) ≝
     305and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (region × block × int × trace) ≝
    306306match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    307307
Note: See TracChangeset for help on using the changeset viewer.