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/lIN_semantics.ml

    r2829 r2951  
    2727open IO
    2828
     29open Joint_semantics
     30
     31open SemanticsUtils
     32
    2933open Extra_bool
    3034
     
    4044
    4145open Globalenvs
    42 
    43 open Joint_semantics
    44 
    45 open SemanticsUtils
    4646
    4747open String
     
    160160    (Joint.lp_to_p__o__stmt_pars__o__uns_pars LIN.lIN);
    161161    SemanticsUtils.slp_sup = (fun _ ->
    162     Joint_LTL_LIN_semantics.lTL_LIN_semantics) }
     162    Joint_LTL_LIN_semantics.lTL_LIN_semantics);
     163    SemanticsUtils.lin_pre_main_generator = LIN.lIN_premain }
    163164
Note: See TracChangeset for help on using the changeset viewer.