Changeset 2951 for extracted/traces.mli


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

    r2829 r2951  
    11open Preamble
    22
     3open ExtraMonads
     4
     5open Deqsets_extra
     6
     7open State
     8
     9open Bind_new
     10
     11open BindLists
     12
     13open Blocks
     14
     15open TranslateUtils
     16
    317open ExtraGlobalenvs
    418
     
    132146
    133147open Joint_semantics
     148
     149open SemanticsUtils
    134150
    135151open StructuredTraces
     
    191207val evaluation_params_jmdiscr : evaluation_params -> evaluation_params -> __
    192208
    193 val sparams__o__msu_pars :
     209val sparams__o__spp' : evaluation_params -> Joint_semantics.serialized_params
     210
     211val sparams__o__spp'__o__msu_pars :
    194212  evaluation_params -> Joint.joint_closed_internal_function
    195213  Joint_semantics.sem_unserialized_params
    196214
    197 val sparams__o__msu_pars__o__st_pars :
     215val sparams__o__spp'__o__msu_pars__o__st_pars :
    198216  evaluation_params -> Joint_semantics.sem_state_params
    199217
    200 val sparams__o__spp : evaluation_params -> Joint.params
    201 
    202 val sparams__o__spp__o__stmt_pars : evaluation_params -> Joint.stmt_params
    203 
    204 val sparams__o__spp__o__stmt_pars__o__uns_pars :
     218val sparams__o__spp'__o__spp : evaluation_params -> Joint.params
     219
     220val sparams__o__spp'__o__spp__o__stmt_pars :
     221  evaluation_params -> Joint.stmt_params
     222
     223val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    205224  evaluation_params -> Joint.uns_params
    206225
    207 val sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     226val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    208227  evaluation_params -> Joint.unserialized_params
    209228
     
    269288  prog_params -> Joint_semantics.sem_params
    270289
    271 val prog_params_to_ev_params__o__sparams__o__msu_pars :
     290val prog_params_to_ev_params__o__sparams__o__spp' :
     291  prog_params -> Joint_semantics.serialized_params
     292
     293val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars :
    272294  prog_params -> Joint.joint_closed_internal_function
    273295  Joint_semantics.sem_unserialized_params
    274296
    275 val prog_params_to_ev_params__o__sparams__o__msu_pars__o__st_pars :
     297val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    276298  prog_params -> Joint_semantics.sem_state_params
    277299
    278 val prog_params_to_ev_params__o__sparams__o__spp :
     300val prog_params_to_ev_params__o__sparams__o__spp'__o__spp :
    279301  prog_params -> Joint.params
    280302
    281 val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars :
     303val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars :
    282304  prog_params -> Joint.stmt_params
    283305
    284 val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
     306val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    285307  prog_params -> Joint.uns_params
    286308
    287 val prog_params_to_ev_params__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     309val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    288310  prog_params -> Joint.unserialized_params
    289311
    290 val make_initial_state : prog_params -> Joint_semantics.state_pc Errors.res
     312val make_initial_state : prog_params -> Joint_semantics.state_pc
    291313
    292314val joint_classify_step :
     
    316338  Types.option
    317339
     340val exit_pc' : ByteValues.program_counter
     341
     342val joint_final :
     343  Joint_semantics.sem_params -> AST.ident List.list -> Joint_semantics.genv
     344  -> Joint_semantics.state_pc -> Integers.int Types.option
     345
    318346val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
    319347
Note: See TracChangeset for help on using the changeset viewer.