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/compiler.mli

    r2909 r2951  
    149149open ToCminor
    150150
    151 open Initialisation
    152 
    153151open BitVectorTrie
    154152
     
    172170
    173171open CostCheck
    174 
    175 open Executions
    176 
    177 open StructuredTraces
    178 
    179 open RTLabs_semantics
    180 
    181 open RTLabs_abstract
    182 
    183 open RTLabs_traces
    184172
    185173open CostInj
     
    338326
    339327val back_end :
    340   observe_pass -> RTLabs_syntax.rTLabs_program ->
     328  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    341329  ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
    342330  Types.prod Errors.res
     
    357345  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
    358346  Errors.res
     347
     348open StructuredTraces
    359349
    360350open AbstractStatus
Note: See TracChangeset for help on using the changeset viewer.