Changeset 2960 for extracted/traces.mli


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/traces.mli

    r2951 r2960  
    152152
    153153type evaluation_params = { globals : AST.ident List.list;
    154                            sparams : Joint_semantics.sem_params;
    155154                           ev_genv : Joint_semantics.genv }
    156155
    157156val evaluation_params_rect_Type4 :
    158   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     157  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    159158  -> 'a1) -> evaluation_params -> 'a1
    160159
    161160val evaluation_params_rect_Type5 :
    162   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     161  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    163162  -> 'a1) -> evaluation_params -> 'a1
    164163
    165164val evaluation_params_rect_Type3 :
    166   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     165  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    167166  -> 'a1) -> evaluation_params -> 'a1
    168167
    169168val evaluation_params_rect_Type2 :
    170   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     169  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    171170  -> 'a1) -> evaluation_params -> 'a1
    172171
    173172val evaluation_params_rect_Type1 :
    174   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     173  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    175174  -> 'a1) -> evaluation_params -> 'a1
    176175
    177176val evaluation_params_rect_Type0 :
    178   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
    179   -> 'a1) -> evaluation_params -> 'a1
    180 
    181 val globals : evaluation_params -> AST.ident List.list
    182 
    183 val sparams : evaluation_params -> Joint_semantics.sem_params
    184 
    185 val ev_genv : evaluation_params -> Joint_semantics.genv
     177  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
     178  -> 'a1) -> evaluation_params -> 'a1
     179
     180val globals :
     181  Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list
     182
     183val ev_genv :
     184  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
    186185
    187186val evaluation_params_inv_rect_Type4 :
    188   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     187  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    189188  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    190189
    191190val evaluation_params_inv_rect_Type3 :
    192   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     191  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    193192  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    194193
    195194val evaluation_params_inv_rect_Type2 :
    196   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     195  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    197196  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    198197
    199198val evaluation_params_inv_rect_Type1 :
    200   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     199  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    201200  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    202201
    203202val evaluation_params_inv_rect_Type0 :
    204   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
    205   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    206 
    207 val evaluation_params_jmdiscr : evaluation_params -> evaluation_params -> __
    208 
    209 val sparams__o__spp' : evaluation_params -> Joint_semantics.serialized_params
    210 
    211 val sparams__o__spp'__o__msu_pars :
    212   evaluation_params -> Joint.joint_closed_internal_function
    213   Joint_semantics.sem_unserialized_params
    214 
    215 val sparams__o__spp'__o__msu_pars__o__st_pars :
    216   evaluation_params -> Joint_semantics.sem_state_params
    217 
    218 val sparams__o__spp'__o__spp : evaluation_params -> Joint.params
    219 
    220 val sparams__o__spp'__o__spp__o__stmt_pars :
    221   evaluation_params -> Joint.stmt_params
    222 
    223 val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    224   evaluation_params -> Joint.uns_params
    225 
    226 val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    227   evaluation_params -> Joint.unserialized_params
     203  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
     204  Joint_semantics.genv -> __ -> 'a1) -> 'a1
     205
     206val evaluation_params_discr :
     207  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
     208
     209val evaluation_params_jmdiscr :
     210  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
     211
     212val dpi1__o__ev_genv__o__inject :
     213  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     214  Joint_semantics.genv Types.sig0
     215
     216val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject :
     217  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     218  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     219  Types.sig0
     220
     221val dpi1__o__ev_genv__o__genv_to_genv_t :
     222  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     223  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     224
     225val eject__o__ev_genv__o__inject :
     226  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     227  Joint_semantics.genv Types.sig0
     228
     229val eject__o__ev_genv__o__genv_to_genv_t__o__inject :
     230  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     231  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     232  Types.sig0
     233
     234val eject__o__ev_genv__o__genv_to_genv_t :
     235  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     236  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     237
     238val ev_genv__o__genv_to_genv_t :
     239  Joint_semantics.sem_params -> evaluation_params ->
     240  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     241
     242val ev_genv__o__genv_to_genv_t__o__inject :
     243  Joint_semantics.sem_params -> evaluation_params ->
     244  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     245  Types.sig0
     246
     247val ev_genv__o__inject :
     248  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
     249  Types.sig0
     250
     251val dpi1__o__ev_genv :
     252  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     253  Joint_semantics.genv
     254
     255val eject__o__ev_genv :
     256  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     257  Joint_semantics.genv
    228258
    229259type prog_params = { prog_spars : Joint_semantics.sem_params;
     
    283313val prog_params_jmdiscr : prog_params -> prog_params -> __
    284314
    285 val make_global : prog_params -> evaluation_params
    286 
    287 val prog_params_to_ev_params__o__sparams :
    288   prog_params -> Joint_semantics.sem_params
    289 
    290 val prog_params_to_ev_params__o__sparams__o__spp' :
    291   prog_params -> Joint_semantics.serialized_params
    292 
    293 val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars :
     315val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params
     316
     317val prog_spars__o__spp'__o__msu_pars :
    294318  prog_params -> Joint.joint_closed_internal_function
    295319  Joint_semantics.sem_unserialized_params
    296320
    297 val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :
     321val prog_spars__o__spp'__o__msu_pars__o__st_pars :
    298322  prog_params -> Joint_semantics.sem_state_params
    299323
    300 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp :
    301   prog_params -> Joint.params
    302 
    303 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars :
     324val prog_spars__o__spp'__o__spp : prog_params -> Joint.params
     325
     326val prog_spars__o__spp'__o__spp__o__stmt_pars :
    304327  prog_params -> Joint.stmt_params
    305328
    306 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
     329val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    307330  prog_params -> Joint.uns_params
    308331
    309 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     332val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    310333  prog_params -> Joint.unserialized_params
    311334
     335val joint_make_global : prog_params -> evaluation_params
     336
     337val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv
     338
     339val joint_make_global__o__ev_genv__o__genv_to_genv_t :
     340  prog_params -> Joint.joint_closed_internal_function AST.fundef
     341  Globalenvs.genv_t
     342
     343val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject :
     344  prog_params -> Joint.joint_closed_internal_function AST.fundef
     345  Globalenvs.genv_t Types.sig0
     346
     347val joint_make_global__o__ev_genv__o__inject :
     348  prog_params -> Joint_semantics.genv Types.sig0
     349
     350val joint_make_global__o__inject :
     351  prog_params -> evaluation_params Types.sig0
     352
    312353val make_initial_state : prog_params -> Joint_semantics.state_pc
    313354
    314355val joint_classify_step :
    315   evaluation_params -> Joint.joint_step -> StructuredTraces.status_class
     356  Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
     357  StructuredTraces.status_class
    316358
    317359val joint_classify_final :
    318   evaluation_params -> Joint.joint_fin_step -> StructuredTraces.status_class
     360  Joint.unserialized_params -> Joint.joint_fin_step ->
     361  StructuredTraces.status_class
    319362
    320363val joint_classify :
    321   evaluation_params -> Joint_semantics.state_pc ->
    322   StructuredTraces.status_class
     364  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     365  -> StructuredTraces.status_class
    323366
    324367val joint_call_ident :
    325   evaluation_params -> Joint_semantics.state_pc -> AST.ident
     368  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     369  -> AST.ident
    326370
    327371val joint_tailcall_ident :
    328   evaluation_params -> Joint_semantics.state_pc -> AST.ident
     372  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     373  -> AST.ident
    329374
    330375val pcDeq : Deqsets.deqSet
    331376
    332377val cost_label_of_stmt :
    333   evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
    334   Types.option
     378  Joint_semantics.sem_params -> evaluation_params -> Joint.joint_statement ->
     379  CostLabel.costlabel Types.option
    335380
    336381val joint_label_of_pc :
    337   evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
    338   Types.option
     382  Joint_semantics.sem_params -> evaluation_params ->
     383  ByteValues.program_counter -> CostLabel.costlabel Types.option
    339384
    340385val exit_pc' : ByteValues.program_counter
    341386
    342387val joint_final :
    343   Joint_semantics.sem_params -> AST.ident List.list -> Joint_semantics.genv
    344   -> Joint_semantics.state_pc -> Integers.int Types.option
     388  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     389  -> Integers.int Types.option
    345390
    346391val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
Note: See TracChangeset for help on using the changeset viewer.