Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 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/rTLabs_abstract.ml

    r2903 r2951  
    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_17605 =
    153   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17605 in
     152let 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
    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_17607 =
    160   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17607 in
     159let 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
    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_17609 =
    167   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17609 in
     166let 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
    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_17611 =
    174   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17611 in
     173let 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
    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_17613 =
    181   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17613 in
     180let 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
    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_17615 =
    188   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17615 in
     187let 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
    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_17641, x_17640) -> h_rapc_state x_17641 x_17640
    343 | Rapc_call (x_17643, x_17642) -> h_rapc_call x_17643 x_17642
    344 | Rapc_ret x_17644 -> h_rapc_ret x_17644
     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
    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_17651, x_17650) -> h_rapc_state x_17651 x_17650
    353 | Rapc_call (x_17653, x_17652) -> h_rapc_call x_17653 x_17652
    354 | Rapc_ret x_17654 -> h_rapc_ret x_17654
     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
    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_17661, x_17660) -> h_rapc_state x_17661 x_17660
    363 | Rapc_call (x_17663, x_17662) -> h_rapc_call x_17663 x_17662
    364 | Rapc_ret x_17664 -> h_rapc_ret x_17664
     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
    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_17671, x_17670) -> h_rapc_state x_17671 x_17670
    373 | Rapc_call (x_17673, x_17672) -> h_rapc_call x_17673 x_17672
    374 | Rapc_ret x_17674 -> h_rapc_ret x_17674
     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
    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_17681, x_17680) -> h_rapc_state x_17681 x_17680
    383 | Rapc_call (x_17683, x_17682) -> h_rapc_call x_17683 x_17682
    384 | Rapc_ret x_17684 -> h_rapc_ret x_17684
     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
    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_17691, x_17690) -> h_rapc_state x_17691 x_17690
    393 | Rapc_call (x_17693, x_17692) -> h_rapc_call x_17693 x_17692
    394 | Rapc_ret x_17694 -> h_rapc_ret x_17694
     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
    395395| Rapc_fin -> h_rapc_fin
    396396
Note: See TracChangeset for help on using the changeset viewer.