Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.mli

    r2890 r2951  
    2626
    2727open Util
     28
     29open Extra_bool
     30
     31open Coqlib
     32
     33open Values
     34
     35open FrontEndVal
     36
     37open GenMem
     38
     39open FrontEndMem
     40
     41open Globalenvs
    2842
    2943open String
     
    113127open Fixpoints
    114128
     129val rl_included :
     130  (PreIdentifiers.identifier Set_adt.set, I8051.register Set_adt.set)
     131  Types.prod -> (PreIdentifiers.identifier Set_adt.set, I8051.register
     132  Set_adt.set) Types.prod -> Bool.bool
     133
    115134val register_lattice : Fixpoints.property_lattice
    116135
     
    149168
    150169val livebefore :
    151   AST.ident List.list -> Joint.joint_internal_function ->
    152   PreIdentifiers.identifier -> Fixpoints.valuation -> __
     170  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
     171  -> Fixpoints.valuation
    153172
    154173val liveafter :
     
    158177val analyse_liveness :
    159178  Fixpoints.fixpoint_computer -> AST.ident List.list ->
    160   Joint.joint_internal_function -> Fixpoints.valuation
     179  Joint.joint_internal_function -> Fixpoints.fixpoint
    161180
    162181type vertex = (Registers.register, I8051.register) Types.sum
Note: See TracChangeset for help on using the changeset viewer.