Changeset 2905 for src/semantics.ma


Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (8 years ago)
Author:
sacerdot
Message:

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/semantics.ma

    r2899 r2905  
    4040  | assembly_pass ⇒
    4141     λprog. let 〈code,sigma,policy〉 ≝ prog in
    42       mk_preclassified_system_pass … (ASM_preclassified_system prog sigma policy) …
     42      mk_preclassified_system_pass … (ASM_preclassified_system code sigma policy) …
    4343  | object_code_pass ⇒
    4444     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
Note: See TracChangeset for help on using the changeset viewer.