Changeset 2905 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (7 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/ASM/Interpret2.ma

    r2899 r2905  
    122122 λc,sigma,policy.
    123123  mk_preclassified_system_of_abstract_status
    124    pseudo_assembly_program
     124   (pseudo_assembly_program × (Word → Word) × (Word → bool))
    125125   (ASM_abstract_status c sigma policy)
    126126   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
Note: See TracChangeset for help on using the changeset viewer.