Changeset 2899 for src/semantics.ma

Timestamp:

Mar 19, 2013, 12:33:13 AM (7 years ago)

Author:

sacerdot

Message:

1. some renaming ASM_xxx to OC_xxx
2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.

File:

• src/semantics.ma (modified) (1 diff)

src/semantics.ma

@@ -39 +39 @@
      λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
   | assembly_pass ⇒
-     ?
+     λprog. let 〈code,sigma,policy〉 ≝ prog in
+      mk_preclassified_system_pass … (ASM_preclassified_system prog sigma policy) …
   | object_code_pass ⇒
      λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
   ].
-try % cases daemon
+%
 qed.