Changeset 1139 for src/Clight/Csem.ma

Timestamp:

Aug 30, 2011, 12:47:18 PM (10 years ago)

Author:

campbell

Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:

• src/Clight/Csem.ma (modified) (2 diffs)

src/Clight/Csem.ma

@@ -1511 +1511 @@
 inductive initial_state (p: clight_program): state -> Prop :=
   | initial_state_intro: ∀b,f,ge,m0.
-      globalenv Genv ?? p = OK ? ge →
-      init_mem Genv ?? p = OK ? m0 →
+      globalenv Genv ?? (fst ??) p = OK ? ge →
+      init_mem Genv ?? (fst ??) p = OK ? m0 →
       find_symbol ?? ge (prog_main ?? p) = Some ? b →
       find_funct_ptr ?? ge b = Some ? f →
@@ -1529 +1529 @@
 
 definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
-  ∀ge. globalenv ??? p = OK ? ge →
+  ∀ge. globalenv ??? (fst ??) p = OK ? ge →
   program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.
 (*