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/ASMCostsSplit.ma

    r2760 r2899  
    331331  ∀p: labelled_object_code.
    332332  let code_memory ≝ load_code_memory (oc p) in
    333   let a_s ≝ ASM_abstract_status code_memory (costlabels p) in
     333  let a_s ≝ OC_abstract_status code_memory (costlabels p) in
    334334  as_cost_map a_s ≝
    335335  λp.
Note: See TracChangeset for help on using the changeset viewer.