Changeset 2899 for src/ASM/AssemblyProofSplitSplit.ma

Timestamp:

Mar 19, 2013, 12:33:13 AM (8 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/ASM/AssemblyProofSplitSplit.ma (modified) (1 diff)

src/ASM/AssemblyProofSplitSplit.ma

@@ -45 +45 @@
       ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
         status_of_pseudo_status M' … 
-          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
+          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
     #M #M' * #preamble #instr_list #program_in_bounds
     @pair_elim #labels #cost #create_label_cost_refl