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

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2278 r2899  
    4545      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    4646        status_of_pseudo_status M' …
    47           (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
     47          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
    4848    #M #M' * #preamble #instr_list #program_in_bounds
    4949    @pair_elim #labels #cost #create_label_cost_refl
Note: See TracChangeset for help on using the changeset viewer.