Changeset 2264 for src/ASM/PolicyStep.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2248 r2264  
    10671067    occurs_exactly_once ?? l program →
    10681068    bitvector_of_nat ? (lookup_def … lm l 0) =
    1069     address_of_word_labels_code_mem program l).
     1069    address_of_word_labels program l).
    10701070  ∀old_policy:(Σpolicy:ppc_pc_map.
    10711071    (* out_of_program_none program policy *)
Note: See TracChangeset for help on using the changeset viewer.