Changeset 2264 for src/ASM/PolicyStep.ma

Timestamp:

Jul 26, 2012, 12:38:42 AM (8 years ago)

Author:

sacerdot

Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:

• src/ASM/PolicyStep.ma (modified) (1 diff)

src/ASM/PolicyStep.ma

@@ -1067 +1067 @@
     occurs_exactly_once ?? l program →
     bitvector_of_nat ? (lookup_def … lm l 0) =
-    address_of_word_labels_code_mem program l).
+    address_of_word_labels program l).
   ∀old_policy:(Σpolicy:ppc_pc_map.
     (* out_of_program_none program policy *)