Changeset 2899 for src/semantics.ma


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

    r2875 r2899  
    3939     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
    4040  | assembly_pass ⇒
    41      ?
     41     λprog. let 〈code,sigma,policy〉 ≝ prog in
     42      mk_preclassified_system_pass … (ASM_preclassified_system prog sigma policy) …
    4243  | object_code_pass ⇒
    4344     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
    4445  ].
    45 try % cases daemon
     46%
    4647qed.
    4748
Note: See TracChangeset for help on using the changeset viewer.