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

    r2951 r2960  
    160160
    161161open Measurable
    162 
    163 type joint_global = { jglobals : AST.ident List.list;
    164                       jgenv : Joint_semantics.genv }
    165 
    166 (** val joint_global_rect_Type4 :
    167     Joint_semantics.sem_params -> (AST.ident List.list ->
    168     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    169 let rec joint_global_rect_Type4 p h_mk_joint_global x_6006 =
    170   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6006 in
    171   h_mk_joint_global jglobals0 jgenv0
    172 
    173 (** val joint_global_rect_Type5 :
    174     Joint_semantics.sem_params -> (AST.ident List.list ->
    175     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    176 let rec joint_global_rect_Type5 p h_mk_joint_global x_6008 =
    177   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6008 in
    178   h_mk_joint_global jglobals0 jgenv0
    179 
    180 (** val joint_global_rect_Type3 :
    181     Joint_semantics.sem_params -> (AST.ident List.list ->
    182     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    183 let rec joint_global_rect_Type3 p h_mk_joint_global x_6010 =
    184   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6010 in
    185   h_mk_joint_global jglobals0 jgenv0
    186 
    187 (** val joint_global_rect_Type2 :
    188     Joint_semantics.sem_params -> (AST.ident List.list ->
    189     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    190 let rec joint_global_rect_Type2 p h_mk_joint_global x_6012 =
    191   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6012 in
    192   h_mk_joint_global jglobals0 jgenv0
    193 
    194 (** val joint_global_rect_Type1 :
    195     Joint_semantics.sem_params -> (AST.ident List.list ->
    196     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    197 let rec joint_global_rect_Type1 p h_mk_joint_global x_6014 =
    198   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6014 in
    199   h_mk_joint_global jglobals0 jgenv0
    200 
    201 (** val joint_global_rect_Type0 :
    202     Joint_semantics.sem_params -> (AST.ident List.list ->
    203     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    204 let rec joint_global_rect_Type0 p h_mk_joint_global x_6016 =
    205   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6016 in
    206   h_mk_joint_global jglobals0 jgenv0
    207 
    208 (** val jglobals :
    209     Joint_semantics.sem_params -> joint_global -> AST.ident List.list **)
    210 let rec jglobals p xxx =
    211   xxx.jglobals
    212 
    213 (** val jgenv :
    214     Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv **)
    215 let rec jgenv p xxx =
    216   xxx.jgenv
    217 
    218 (** val joint_global_inv_rect_Type4 :
    219     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    220     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    221 let joint_global_inv_rect_Type4 x1 hterm h1 =
    222   let hcut = joint_global_rect_Type4 x1 h1 hterm in hcut __
    223 
    224 (** val joint_global_inv_rect_Type3 :
    225     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    226     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    227 let joint_global_inv_rect_Type3 x1 hterm h1 =
    228   let hcut = joint_global_rect_Type3 x1 h1 hterm in hcut __
    229 
    230 (** val joint_global_inv_rect_Type2 :
    231     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    232     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    233 let joint_global_inv_rect_Type2 x1 hterm h1 =
    234   let hcut = joint_global_rect_Type2 x1 h1 hterm in hcut __
    235 
    236 (** val joint_global_inv_rect_Type1 :
    237     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    238     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    239 let joint_global_inv_rect_Type1 x1 hterm h1 =
    240   let hcut = joint_global_rect_Type1 x1 h1 hterm in hcut __
    241 
    242 (** val joint_global_inv_rect_Type0 :
    243     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    244     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    245 let joint_global_inv_rect_Type0 x1 hterm h1 =
    246   let hcut = joint_global_rect_Type0 x1 h1 hterm in hcut __
    247 
    248 (** val joint_global_discr :
    249     Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
    250 let joint_global_discr a1 x y =
    251   Logic.eq_rect_Type2 x
    252     (let { jglobals = a0; jgenv = a10 } = x in
    253     Obj.magic (fun _ dH -> dH __ __)) y
    254 
    255 (** val joint_global_jmdiscr :
    256     Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
    257 let joint_global_jmdiscr a1 x y =
    258   Logic.eq_rect_Type2 x
    259     (let { jglobals = a0; jgenv = a10 } = x in
    260     Obj.magic (fun _ dH -> dH __ __)) y
    261 
    262 (** val dpi1__o__jgenv__o__inject :
    263     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    264     Joint_semantics.genv Types.sig0 **)
    265 let dpi1__o__jgenv__o__inject x0 x2 =
    266   x2.Types.dpi1.jgenv
    267 
    268 (** val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
    269     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    270     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    271     Types.sig0 **)
    272 let dpi1__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
    273   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    274     x2.Types.dpi1.jglobals x2.Types.dpi1.jgenv
    275 
    276 (** val dpi1__o__jgenv__o__genv_to_genv_t :
    277     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    278     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    279 let dpi1__o__jgenv__o__genv_to_genv_t x0 x2 =
    280   let p = Joint_semantics.spp'__o__spp x0 in
    281   let globals = x2.Types.dpi1.jglobals in
    282   let g = x2.Types.dpi1.jgenv in g.Joint_semantics.ge
    283 
    284 (** val eject__o__jgenv__o__inject :
    285     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    286     Joint_semantics.genv Types.sig0 **)
    287 let eject__o__jgenv__o__inject x0 x2 =
    288   (Types.pi1 x2).jgenv
    289 
    290 (** val eject__o__jgenv__o__genv_to_genv_t__o__inject :
    291     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    292     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    293     Types.sig0 **)
    294 let eject__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
    295   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    296     (Types.pi1 x2).jglobals (Types.pi1 x2).jgenv
    297 
    298 (** val eject__o__jgenv__o__genv_to_genv_t :
    299     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    300     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    301 let eject__o__jgenv__o__genv_to_genv_t x0 x2 =
    302   let p = Joint_semantics.spp'__o__spp x0 in
    303   let globals = (Types.pi1 x2).jglobals in
    304   let g = (Types.pi1 x2).jgenv in g.Joint_semantics.ge
    305 
    306 (** val jgenv__o__genv_to_genv_t :
    307     Joint_semantics.sem_params -> joint_global ->
    308     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    309 let jgenv__o__genv_to_genv_t x0 x1 =
    310   let p = Joint_semantics.spp'__o__spp x0 in
    311   let globals = x1.jglobals in let g = x1.jgenv in g.Joint_semantics.ge
    312 
    313 (** val jgenv__o__genv_to_genv_t__o__inject :
    314     Joint_semantics.sem_params -> joint_global ->
    315     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    316     Types.sig0 **)
    317 let jgenv__o__genv_to_genv_t__o__inject x0 x1 =
    318   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    319     x1.jglobals x1.jgenv
    320 
    321 (** val jgenv__o__inject :
    322     Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    323     Types.sig0 **)
    324 let jgenv__o__inject x0 x1 =
    325   x1.jgenv
    326 
    327 (** val dpi1__o__jgenv :
    328     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    329     Joint_semantics.genv **)
    330 let dpi1__o__jgenv x0 x2 =
    331   x2.Types.dpi1.jgenv
    332 
    333 (** val eject__o__jgenv :
    334     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    335     Joint_semantics.genv **)
    336 let eject__o__jgenv x0 x2 =
    337   (Types.pi1 x2).jgenv
    338 
    339 (** val eval_params_of_global :
    340     Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params **)
    341 let eval_params_of_global p gl =
    342   { Traces.globals = gl.jglobals; Traces.sparams = p; Traces.ev_genv =
    343     gl.jgenv }
    344 
    345 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    346     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    347     Joint.unserialized_params **)
    348 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
    349   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    350     (eval_params_of_global x0 x2.Types.dpi1)
    351 
    352 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    353     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    354     Joint.uns_params **)
    355 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
    356   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    357     (eval_params_of_global x0 x2.Types.dpi1)
    358 
    359 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    360     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    361     Joint.stmt_params **)
    362 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
    363   Traces.sparams__o__spp'__o__spp__o__stmt_pars
    364     (eval_params_of_global x0 x2.Types.dpi1)
    365 
    366 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    367     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    368     Joint.params **)
    369 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
    370   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x2.Types.dpi1)
    371 
    372 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    373     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    374     Joint_semantics.sem_state_params **)
    375 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
    376   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    377     (eval_params_of_global x0 x2.Types.dpi1)
    378 
    379 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    380     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    381     Joint.joint_closed_internal_function
    382     Joint_semantics.sem_unserialized_params **)
    383 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
    384   Traces.sparams__o__spp'__o__msu_pars
    385     (eval_params_of_global x0 x2.Types.dpi1)
    386 
    387 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp' :
    388     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    389     Joint_semantics.serialized_params **)
    390 let dpi1__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
    391   Traces.sparams__o__spp' (eval_params_of_global x0 x2.Types.dpi1)
    392 
    393 (** val dpi1__o__eval_params_of_global__o__sparams :
    394     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    395     Joint_semantics.sem_params **)
    396 let dpi1__o__eval_params_of_global__o__sparams x0 x2 =
    397   (eval_params_of_global x0 x2.Types.dpi1).Traces.sparams
    398 
    399 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    400     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    401     Joint.unserialized_params **)
    402 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
    403   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    404     (eval_params_of_global x0 (Types.pi1 x2))
    405 
    406 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    407     Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params **)
    408 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
    409   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    410     (eval_params_of_global x0 (Types.pi1 x2))
    411 
    412 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    413     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    414     Joint.stmt_params **)
    415 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
    416   Traces.sparams__o__spp'__o__spp__o__stmt_pars
    417     (eval_params_of_global x0 (Types.pi1 x2))
    418 
    419 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    420     Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params **)
    421 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
    422   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 (Types.pi1 x2))
    423 
    424 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    425     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    426     Joint_semantics.sem_state_params **)
    427 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
    428   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    429     (eval_params_of_global x0 (Types.pi1 x2))
    430 
    431 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    432     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    433     Joint.joint_closed_internal_function
    434     Joint_semantics.sem_unserialized_params **)
    435 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
    436   Traces.sparams__o__spp'__o__msu_pars
    437     (eval_params_of_global x0 (Types.pi1 x2))
    438 
    439 (** val eject__o__eval_params_of_global__o__sparams__o__spp' :
    440     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    441     Joint_semantics.serialized_params **)
    442 let eject__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
    443   Traces.sparams__o__spp' (eval_params_of_global x0 (Types.pi1 x2))
    444 
    445 (** val eject__o__eval_params_of_global__o__sparams :
    446     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    447     Joint_semantics.sem_params **)
    448 let eject__o__eval_params_of_global__o__sparams x0 x2 =
    449   (eval_params_of_global x0 (Types.pi1 x2)).Traces.sparams
    450 
    451 (** val eval_params_of_global__o__sparams :
    452     Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params **)
    453 let eval_params_of_global__o__sparams x0 x1 =
    454   (eval_params_of_global x0 x1).Traces.sparams
    455 
    456 (** val eval_params_of_global__o__sparams__o__spp' :
    457     Joint_semantics.sem_params -> joint_global ->
    458     Joint_semantics.serialized_params **)
    459 let eval_params_of_global__o__sparams__o__spp' x0 x1 =
    460   Traces.sparams__o__spp' (eval_params_of_global x0 x1)
    461 
    462 (** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    463     Joint_semantics.sem_params -> joint_global ->
    464     Joint.joint_closed_internal_function
    465     Joint_semantics.sem_unserialized_params **)
    466 let eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x1 =
    467   Traces.sparams__o__spp'__o__msu_pars (eval_params_of_global x0 x1)
    468 
    469 (** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    470     Joint_semantics.sem_params -> joint_global ->
    471     Joint_semantics.sem_state_params **)
    472 let eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x1 =
    473   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    474     (eval_params_of_global x0 x1)
    475 
    476 (** val eval_params_of_global__o__sparams__o__spp'__o__spp :
    477     Joint_semantics.sem_params -> joint_global -> Joint.params **)
    478 let eval_params_of_global__o__sparams__o__spp'__o__spp x0 x1 =
    479   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x1)
    480 
    481 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    482     Joint_semantics.sem_params -> joint_global -> Joint.stmt_params **)
    483 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x1 =
    484   Traces.sparams__o__spp'__o__spp__o__stmt_pars (eval_params_of_global x0 x1)
    485 
    486 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    487     Joint_semantics.sem_params -> joint_global -> Joint.uns_params **)
    488 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x1 =
    489   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    490     (eval_params_of_global x0 x1)
    491 
    492 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    493     Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params **)
    494 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x1 =
    495   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    496     (eval_params_of_global x0 x1)
    497 
    498 (** val dpi1__o__eval_params_of_global :
    499     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    500     Traces.evaluation_params **)
    501 let dpi1__o__eval_params_of_global x0 x2 =
    502   eval_params_of_global x0 x2.Types.dpi1
    503 
    504 (** val eject__o__eval_params_of_global :
    505     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    506     Traces.evaluation_params **)
    507 let eject__o__eval_params_of_global x0 x2 =
    508   eval_params_of_global x0 (Types.pi1 x2)
    509 
    510 (** val make_joint_global :
    511     Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
    512     Types.option) Types.prod -> joint_global **)
    513 let make_joint_global pars p_stack =
    514   let p = p_stack.Types.fst in
    515   let stack_sizes = p_stack.Types.snd in
    516   let ev_pars =
    517     Traces.make_global { Traces.prog_spars = pars; Traces.prog = p;
    518       Traces.stack_sizes = stack_sizes }
    519   in
    520   { jglobals = ev_pars.Traces.globals; jgenv = ev_pars.Traces.ev_genv }
    521162
    522163(** val joint_exec :
     
    525166let joint_exec g =
    526167  { SmallstepExec.is_final = (fun env ->
    527     Obj.magic
    528       (Traces.joint_final g (Obj.magic env).jglobals (Obj.magic env).jgenv));
    529     SmallstepExec.step = (fun env st ->
     168    Obj.magic (Traces.joint_final g (Obj.magic env))); SmallstepExec.step =
     169    (fun env st ->
    530170    Obj.magic
    531171      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    532172        (Obj.magic
    533           (Joint_semantics.eval_state g (Obj.magic env).jglobals
    534             (Obj.magic env).jgenv (Obj.magic st))) (fun st' ->
     173          (Joint_semantics.eval_state g (Obj.magic env).Traces.globals
     174            (Obj.magic env).Traces.ev_genv (Obj.magic st))) (fun st' ->
    535175        let charge =
    536           match Traces.joint_label_of_pc
    537                   (eval_params_of_global g (Obj.magic env))
     176          match Traces.joint_label_of_pc g (Obj.magic env)
    538177                  (Obj.magic st).Joint_semantics.pc with
    539178          | Types.None -> Events.e0
     
    548187let joint_fullexec g =
    549188  { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
    550     (Obj.magic (make_joint_global g)); SmallstepExec.make_initial_state =
     189    (fun pr ->
     190    Obj.magic
     191      (Traces.joint_make_global { Traces.prog_spars = g; Traces.prog =
     192        (Obj.magic pr).Types.fst; Traces.stack_sizes =
     193        (Obj.magic pr).Types.snd })); SmallstepExec.make_initial_state =
    551194    (fun p_stacks ->
    552195    Obj.magic
     
    563206    Bool.notb
    564207      (PositiveMap.is_none
    565         (Traces.joint_label_of_pc (eval_params_of_global g (Obj.magic env))
     208        (Traces.joint_label_of_pc g (Obj.magic env)
    566209          (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
    567     (fun env ->
    568     Obj.magic
    569       (Traces.joint_classify (eval_params_of_global g (Obj.magic env))));
     210    (fun env -> Obj.magic (Traces.joint_classify g (Obj.magic env)));
    570211    Measurable.pcs_callee = (fun env s _ ->
    571     Traces.joint_call_ident (eval_params_of_global g (Obj.magic env))
    572       (Obj.magic s)) }
    573 
     212    Traces.joint_call_ident g (Obj.magic env) (Obj.magic s)) }
     213
Note: See TracChangeset for help on using the changeset viewer.