Changeset 2709


Ignore:
Timestamp:
Feb 22, 2013, 7:17:44 PM (6 years ago)
Author:
sacerdot
Message:

LINToAsm repaired

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2705 r2709  
    2020include "ERTLptr/ERTLptrToLTL.ma".
    2121include "LTL/LTLToLIN.ma".
    22 (*
    2322include "LIN/LINToASM.ma".
    24 *) include "ASM/ASM.ma".
    25    axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2623
    2724axiom compute_fixpoint : fixpoint_computer.
     
    3734          lin_to_asm p.
    3835
    39 (* JHM: minimum needed for assembler axiom to typecheck *)
    40 (* JHM: moved from ASMCostsSplit.ma                     *)
    41 (* JHM: should move elsewhere in ASM/                   *)
     36(* JHM: minimum needed for assembler to typecheck *)
     37(* JHM: moved from ASMCostsSplit.ma               *)
     38(* JHM: should move elsewhere in ASM/             *)
    4239definition object_code ≝ list Byte.
    4340definition costlabel_map ≝ BitVectorTrie costlabel 16.
Note: See TracChangeset for help on using the changeset viewer.