Changeset 3019 for extracted/traces.ml


Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/traces.ml

    r3001 r3019  
    157157    Joint_semantics.sem_params -> (AST.ident List.list ->
    158158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_15969 =
    160   let { globals = globals0; ev_genv = ev_genv0 } = x_15969 in
     159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_316 =
     160  let { globals = globals0; ev_genv = ev_genv0 } = x_316 in
    161161  h_mk_evaluation_params globals0 ev_genv0
    162162
     
    164164    Joint_semantics.sem_params -> (AST.ident List.list ->
    165165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_15971 =
    167   let { globals = globals0; ev_genv = ev_genv0 } = x_15971 in
     166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_318 =
     167  let { globals = globals0; ev_genv = ev_genv0 } = x_318 in
    168168  h_mk_evaluation_params globals0 ev_genv0
    169169
     
    171171    Joint_semantics.sem_params -> (AST.ident List.list ->
    172172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_15973 =
    174   let { globals = globals0; ev_genv = ev_genv0 } = x_15973 in
     173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_320 =
     174  let { globals = globals0; ev_genv = ev_genv0 } = x_320 in
    175175  h_mk_evaluation_params globals0 ev_genv0
    176176
     
    178178    Joint_semantics.sem_params -> (AST.ident List.list ->
    179179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_15975 =
    181   let { globals = globals0; ev_genv = ev_genv0 } = x_15975 in
     180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_322 =
     181  let { globals = globals0; ev_genv = ev_genv0 } = x_322 in
    182182  h_mk_evaluation_params globals0 ev_genv0
    183183
     
    185185    Joint_semantics.sem_params -> (AST.ident List.list ->
    186186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_15977 =
    188   let { globals = globals0; ev_genv = ev_genv0 } = x_15977 in
     187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_324 =
     188  let { globals = globals0; ev_genv = ev_genv0 } = x_324 in
    189189  h_mk_evaluation_params globals0 ev_genv0
    190190
     
    192192    Joint_semantics.sem_params -> (AST.ident List.list ->
    193193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_15979 =
    195   let { globals = globals0; ev_genv = ev_genv0 } = x_15979 in
     194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_326 =
     195  let { globals = globals0; ev_genv = ev_genv0 } = x_326 in
    196196  h_mk_evaluation_params globals0 ev_genv0
    197197
     
    336336    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    337337    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    338 let rec prog_params_rect_Type4 h_mk_prog_params x_15995 =
     338let rec prog_params_rect_Type4 h_mk_prog_params x_342 =
    339339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    340     stack_sizes0 } = x_15995
     340    stack_sizes0 } = x_342
    341341  in
    342342  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    345345    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    346346    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    347 let rec prog_params_rect_Type5 h_mk_prog_params x_15997 =
     347let rec prog_params_rect_Type5 h_mk_prog_params x_344 =
    348348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    349     stack_sizes0 } = x_15997
     349    stack_sizes0 } = x_344
    350350  in
    351351  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    354354    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    355355    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    356 let rec prog_params_rect_Type3 h_mk_prog_params x_15999 =
     356let rec prog_params_rect_Type3 h_mk_prog_params x_346 =
    357357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    358     stack_sizes0 } = x_15999
     358    stack_sizes0 } = x_346
    359359  in
    360360  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    363363    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    364364    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    365 let rec prog_params_rect_Type2 h_mk_prog_params x_16001 =
     365let rec prog_params_rect_Type2 h_mk_prog_params x_348 =
    366366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    367     stack_sizes0 } = x_16001
     367    stack_sizes0 } = x_348
    368368  in
    369369  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    372372    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    373373    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    374 let rec prog_params_rect_Type1 h_mk_prog_params x_16003 =
     374let rec prog_params_rect_Type1 h_mk_prog_params x_350 =
    375375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    376     stack_sizes0 } = x_16003
     376    stack_sizes0 } = x_350
    377377  in
    378378  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    381381    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    382382    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    383 let rec prog_params_rect_Type0 h_mk_prog_params x_16005 =
     383let rec prog_params_rect_Type0 h_mk_prog_params x_352 =
    384384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    385     stack_sizes0 } = x_16005
     385    stack_sizes0 } = x_352
    386386  in
    387387  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    523523        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    524524          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    525           (Nat.S Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
     525          (Nat.S Nat.O))))))))))))))))
     526          (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
    526527      in
    527528      let main = AST.prog_main p.Joint.joint_prog in
Note: See TracChangeset for help on using the changeset viewer.