Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_abstract.ml

    r2951 r2997  
    150150    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    151151    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_5220 =
    153   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5220 in
     152let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_2496 =
     153  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2496 in
    154154  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    155155
     
    157157    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    158158    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_5222 =
    160   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5222 in
     159let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_2498 =
     160  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2498 in
    161161  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    162162
     
    164164    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    165165    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_5224 =
    167   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5224 in
     166let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_2500 =
     167  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2500 in
    168168  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    169169
     
    171171    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    172172    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_5226 =
    174   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5226 in
     173let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_2502 =
     174  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2502 in
    175175  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    176176
     
    178178    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    179179    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_5228 =
    181   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5228 in
     180let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_2504 =
     181  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2504 in
    182182  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    183183
     
    185185    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    186186    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_5230 =
    188   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_5230 in
     187let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_2506 =
     188  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2506 in
    189189  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    190190
     
    340340    rTLabs_pc -> 'a1 **)
    341341let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    342 | Rapc_state (x_5256, x_5255) -> h_rapc_state x_5256 x_5255
    343 | Rapc_call (x_5258, x_5257) -> h_rapc_call x_5258 x_5257
    344 | Rapc_ret x_5259 -> h_rapc_ret x_5259
     342| Rapc_state (x_2532, x_2531) -> h_rapc_state x_2532 x_2531
     343| Rapc_call (x_2534, x_2533) -> h_rapc_call x_2534 x_2533
     344| Rapc_ret x_2535 -> h_rapc_ret x_2535
    345345| Rapc_fin -> h_rapc_fin
    346346
     
    350350    rTLabs_pc -> 'a1 **)
    351351let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    352 | Rapc_state (x_5266, x_5265) -> h_rapc_state x_5266 x_5265
    353 | Rapc_call (x_5268, x_5267) -> h_rapc_call x_5268 x_5267
    354 | Rapc_ret x_5269 -> h_rapc_ret x_5269
     352| Rapc_state (x_2542, x_2541) -> h_rapc_state x_2542 x_2541
     353| Rapc_call (x_2544, x_2543) -> h_rapc_call x_2544 x_2543
     354| Rapc_ret x_2545 -> h_rapc_ret x_2545
    355355| Rapc_fin -> h_rapc_fin
    356356
     
    360360    rTLabs_pc -> 'a1 **)
    361361let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    362 | Rapc_state (x_5276, x_5275) -> h_rapc_state x_5276 x_5275
    363 | Rapc_call (x_5278, x_5277) -> h_rapc_call x_5278 x_5277
    364 | Rapc_ret x_5279 -> h_rapc_ret x_5279
     362| Rapc_state (x_2552, x_2551) -> h_rapc_state x_2552 x_2551
     363| Rapc_call (x_2554, x_2553) -> h_rapc_call x_2554 x_2553
     364| Rapc_ret x_2555 -> h_rapc_ret x_2555
    365365| Rapc_fin -> h_rapc_fin
    366366
     
    370370    rTLabs_pc -> 'a1 **)
    371371let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    372 | Rapc_state (x_5286, x_5285) -> h_rapc_state x_5286 x_5285
    373 | Rapc_call (x_5288, x_5287) -> h_rapc_call x_5288 x_5287
    374 | Rapc_ret x_5289 -> h_rapc_ret x_5289
     372| Rapc_state (x_2562, x_2561) -> h_rapc_state x_2562 x_2561
     373| Rapc_call (x_2564, x_2563) -> h_rapc_call x_2564 x_2563
     374| Rapc_ret x_2565 -> h_rapc_ret x_2565
    375375| Rapc_fin -> h_rapc_fin
    376376
     
    380380    rTLabs_pc -> 'a1 **)
    381381let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    382 | Rapc_state (x_5296, x_5295) -> h_rapc_state x_5296 x_5295
    383 | Rapc_call (x_5298, x_5297) -> h_rapc_call x_5298 x_5297
    384 | Rapc_ret x_5299 -> h_rapc_ret x_5299
     382| Rapc_state (x_2572, x_2571) -> h_rapc_state x_2572 x_2571
     383| Rapc_call (x_2574, x_2573) -> h_rapc_call x_2574 x_2573
     384| Rapc_ret x_2575 -> h_rapc_ret x_2575
    385385| Rapc_fin -> h_rapc_fin
    386386
     
    390390    rTLabs_pc -> 'a1 **)
    391391let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    392 | Rapc_state (x_5306, x_5305) -> h_rapc_state x_5306 x_5305
    393 | Rapc_call (x_5308, x_5307) -> h_rapc_call x_5308 x_5307
    394 | Rapc_ret x_5309 -> h_rapc_ret x_5309
     392| Rapc_state (x_2582, x_2581) -> h_rapc_state x_2582 x_2581
     393| Rapc_call (x_2584, x_2583) -> h_rapc_call x_2584 x_2583
     394| Rapc_ret x_2585 -> h_rapc_ret x_2585
    395395| Rapc_fin -> h_rapc_fin
    396396
Note: See TracChangeset for help on using the changeset viewer.