Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/abstractStatus.ml

    r2649 r2717  
    44
    55open LabelledObjects
     6
     7open BitVectorTrie
     8
     9open Exp
    610
    711open Arithmetic
     
    7579open ASM
    7680
    77 open BitVectorTrie
    78 
    7981open Status
    8082
     
    127129| ASM.RETI -> StructuredTraces.Cl_return
    128130| ASM.NOP -> StructuredTraces.Cl_other
     131| ASM.JMP x -> StructuredTraces.Cl_call
    129132
    130133(** val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class **)
     
    135138| ASM.LJMP x -> StructuredTraces.Cl_other
    136139| ASM.SJMP x -> StructuredTraces.Cl_other
    137 | ASM.JMP x -> StructuredTraces.Cl_call
    138140| ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
    139141| ASM.RealInstruction pre -> aSM_classify00 pre
Note: See TracChangeset for help on using the changeset viewer.