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

Legend:

Unmodified
Added
Removed
  • src/ASM/AbstractStatus.ma

    r2770 r2899  
    6464qed.
    6565   
    66 definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
     66definition OC_classify: ∀code_memory. Status code_memory → status_class ≝
    6767  λcode_memory.
    6868  λs: Status code_memory.
Note: See TracChangeset for help on using the changeset viewer.