Changeset 1311 for Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

Timestamp:

Oct 6, 2011, 6:45:54 PM (10 years ago)

Author:

campbell

Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• ERTL/semantics.ma (modified) (3 diffs)

Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

@@ -49 +49 @@
 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
 
-definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
+definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
 
 (* CSC: frame reduced to this *)
@@ -139 +139 @@
 
 axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
-axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
+axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
 
 definition init_locals : list register → register_env val ≝
@@ -191 +191 @@
   (* CSC: monadic notation missing here *)
     bind ?? (fetch_function globals st) (λf.
-    OK ? (ertl_if_stacksize globals f)).
+    OK ? (joint_if_stacksize globals … f)).
 
 definition get_hwsp : state → res address ≝