Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 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/toRTLabs.mli

    r2773 r2951  
    647647val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __
    648648
    649 val expr_is_Id : AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
     649val expr_is_cst_ident :
     650  AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
    650651
    651652val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
     
    671672  Cminor_syntax.internal_function -> RTLabs_syntax.internal_function
    672673
    673 val cminor_noinit_to_rtlabs :
    674   Cminor_syntax.cminor_noinit_program -> RTLabs_syntax.rTLabs_program
    675 
    676 open Initialisation
    677 
    678674val cminor_to_rtlabs :
    679   CostLabel.costlabel -> Cminor_syntax.cminor_program ->
    680   RTLabs_syntax.rTLabs_program
    681 
     675  Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program
     676
Note: See TracChangeset for help on using the changeset viewer.