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_traces.ml

    r2873 r2951  
    296296    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    297297    flat_trace -> will_return -> 'a1 **)
    298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17878 s x_17877 = function
    299 | Wr_step (s0, tr, s', depth, trace, x_17880) ->
    300   h_wr_step s0 tr s' depth __ trace __ x_17880
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1409 s x_1408 = function
     299| Wr_step (s0, tr, s', depth, trace, x_1411) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_1411
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    302       s' trace x_17880)
    303 | Wr_call (s0, tr, s', depth, trace, x_17882) ->
    304   h_wr_call s0 tr s' depth __ trace __ x_17882
     302      s' trace x_1411)
     303| Wr_call (s0, tr, s', depth, trace, x_1413) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_1413
    305305    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    306       depth) s' trace x_17882)
    307 | Wr_ret (s0, tr, s', depth, trace, x_17884) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_17884
     306      depth) s' trace x_1413)
     307| Wr_ret (s0, tr, s', depth, trace, x_1415) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_1415
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_17884)
     310      s' trace x_1415)
    311311| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    312312
     
    323323    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    324324    flat_trace -> will_return -> 'a1 **)
    325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17906 s x_17905 = function
    326 | Wr_step (s0, tr, s', depth, trace, x_17908) ->
    327   h_wr_step s0 tr s' depth __ trace __ x_17908
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1437 s x_1436 = function
     326| Wr_step (s0, tr, s', depth, trace, x_1439) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_1439
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    329       s' trace x_17908)
    330 | Wr_call (s0, tr, s', depth, trace, x_17910) ->
    331   h_wr_call s0 tr s' depth __ trace __ x_17910
     329      s' trace x_1439)
     330| Wr_call (s0, tr, s', depth, trace, x_1441) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_1441
    332332    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    333       depth) s' trace x_17910)
    334 | Wr_ret (s0, tr, s', depth, trace, x_17912) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_17912
     333      depth) s' trace x_1441)
     334| Wr_ret (s0, tr, s', depth, trace, x_1443) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_1443
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_17912)
     337      s' trace x_1443)
    338338| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    339339
     
    350350    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    351351    flat_trace -> will_return -> 'a1 **)
    352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17920 s x_17919 = function
    353 | Wr_step (s0, tr, s', depth, trace, x_17922) ->
    354   h_wr_step s0 tr s' depth __ trace __ x_17922
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1451 s x_1450 = function
     353| Wr_step (s0, tr, s', depth, trace, x_1453) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_1453
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    356       s' trace x_17922)
    357 | Wr_call (s0, tr, s', depth, trace, x_17924) ->
    358   h_wr_call s0 tr s' depth __ trace __ x_17924
     356      s' trace x_1453)
     357| Wr_call (s0, tr, s', depth, trace, x_1455) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_1455
    359359    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    360       depth) s' trace x_17924)
    361 | Wr_ret (s0, tr, s', depth, trace, x_17926) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_17926
     360      depth) s' trace x_1455)
     361| Wr_ret (s0, tr, s', depth, trace, x_1457) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_1457
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_17926)
     364      s' trace x_1457)
    365365| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    366366
     
    377377    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    378378    flat_trace -> will_return -> 'a1 **)
    379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17934 s x_17933 = function
    380 | Wr_step (s0, tr, s', depth, trace, x_17936) ->
    381   h_wr_step s0 tr s' depth __ trace __ x_17936
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1465 s x_1464 = function
     380| Wr_step (s0, tr, s', depth, trace, x_1467) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_1467
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    383       s' trace x_17936)
    384 | Wr_call (s0, tr, s', depth, trace, x_17938) ->
    385   h_wr_call s0 tr s' depth __ trace __ x_17938
     383      s' trace x_1467)
     384| Wr_call (s0, tr, s', depth, trace, x_1469) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_1469
    386386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    387       depth) s' trace x_17938)
    388 | Wr_ret (s0, tr, s', depth, trace, x_17940) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_17940
     387      depth) s' trace x_1469)
     388| Wr_ret (s0, tr, s', depth, trace, x_1471) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_1471
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_17940)
     391      s' trace x_1471)
    392392| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    393393
     
    404404    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    405405    flat_trace -> will_return -> 'a1 **)
    406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17948 s x_17947 = function
    407 | Wr_step (s0, tr, s', depth, trace, x_17950) ->
    408   h_wr_step s0 tr s' depth __ trace __ x_17950
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1479 s x_1478 = function
     407| Wr_step (s0, tr, s', depth, trace, x_1481) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_1481
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    410       s' trace x_17950)
    411 | Wr_call (s0, tr, s', depth, trace, x_17952) ->
    412   h_wr_call s0 tr s' depth __ trace __ x_17952
     410      s' trace x_1481)
     411| Wr_call (s0, tr, s', depth, trace, x_1483) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_1483
    413413    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    414       depth) s' trace x_17952)
    415 | Wr_ret (s0, tr, s', depth, trace, x_17954) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_17954
     414      depth) s' trace x_1483)
     415| Wr_ret (s0, tr, s', depth, trace, x_1485) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_1485
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_17954)
     418      s' trace x_1485)
    419419| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    420420
     
    839839    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    840840    trace_result -> 'a2 **)
    841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18489 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2020 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_18489
     843    new_trace0; terminates = terminates0 } = x_2020
    844844  in
    845845  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    851851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    852852    trace_result -> 'a2 **)
    853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18491 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2022 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18491
     855    new_trace0; terminates = terminates0 } = x_2022
    856856  in
    857857  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    863863    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    864864    trace_result -> 'a2 **)
    865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18493 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2024 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18493
     867    new_trace0; terminates = terminates0 } = x_2024
    868868  in
    869869  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    875875    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    876876    trace_result -> 'a2 **)
    877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18495 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2026 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18495
     879    new_trace0; terminates = terminates0 } = x_2026
    880880  in
    881881  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    887887    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    888888    trace_result -> 'a2 **)
    889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18497 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2028 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18497
     891    new_trace0; terminates = terminates0 } = x_2028
    892892  in
    893893  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    899899    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    900900    trace_result -> 'a2 **)
    901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18499 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2030 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18499
     903    new_trace0; terminates = terminates0 } = x_2030
    904904  in
    905905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    999999    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10001000    sub_trace_result -> 'a2 **)
    1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18517 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_18517 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2048 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_2048 in
    10031003  h_mk_sub_trace_result ends0 trace_res0
    10041004
     
    10081008    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10091009    sub_trace_result -> 'a2 **)
    1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18519 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_18519 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2050 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_2050 in
    10121012  h_mk_sub_trace_result ends0 trace_res0
    10131013
     
    10171017    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10181018    sub_trace_result -> 'a2 **)
    1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18521 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_18521 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2052 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_2052 in
    10211021  h_mk_sub_trace_result ends0 trace_res0
    10221022
     
    10261026    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10271027    sub_trace_result -> 'a2 **)
    1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18523 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_18523 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2054 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_2054 in
    10301030  h_mk_sub_trace_result ends0 trace_res0
    10311031
     
    10351035    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10361036    sub_trace_result -> 'a2 **)
    1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18525 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_18525 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2056 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_2056 in
    10391039  h_mk_sub_trace_result ends0 trace_res0
    10401040
     
    10441044    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10451045    sub_trace_result -> 'a2 **)
    1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18527 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_18527 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2058 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_2058 in
    10481048  h_mk_sub_trace_result ends0 trace_res0
    10491049
     
    14721472    (Pointers.block, __) Types.dPair **)
    14731473let init_state_is p s =
    1474   RTLabs_semantics.bind_ok
    1475     (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x), List.Nil))
    1476       p) (fun x ->
     1474  RTLabs_semantics.bind_ok (Globalenvs.init_mem (fun x -> x) p) (fun x ->
    14771475    let main = p.AST.prog_main in
    14781476    Obj.magic
     
    15581556    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15591557    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18862 x_18861 = function
     1558let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function
    15611559| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1562 | Pft_step (s, tr, s', s'', x_18865) ->
    1563   h_pft_step s tr s' s'' __ x_18865
    1564     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18865)
     1560| Pft_step (s, tr, s', s'', x_2396) ->
     1561  h_pft_step s tr s' s'' __ x_2396
     1562    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396)
    15651563
    15661564(** val partial_flat_trace_rect_Type3 :
     
    15701568    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15711569    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18878 x_18877 = function
     1570let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function
    15731571| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1574 | Pft_step (s, tr, s', s'', x_18881) ->
    1575   h_pft_step s tr s' s'' __ x_18881
    1576     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18881)
     1572| Pft_step (s, tr, s', s'', x_2412) ->
     1573  h_pft_step s tr s' s'' __ x_2412
     1574    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412)
    15771575
    15781576(** val partial_flat_trace_rect_Type2 :
     
    15821580    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15831581    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18886 x_18885 = function
     1582let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function
    15851583| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1586 | Pft_step (s, tr, s', s'', x_18889) ->
    1587   h_pft_step s tr s' s'' __ x_18889
    1588     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18889)
     1584| Pft_step (s, tr, s', s'', x_2420) ->
     1585  h_pft_step s tr s' s'' __ x_2420
     1586    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420)
    15891587
    15901588(** val partial_flat_trace_rect_Type1 :
     
    15941592    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15951593    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18894 x_18893 = function
     1594let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function
    15971595| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1598 | Pft_step (s, tr, s', s'', x_18897) ->
    1599   h_pft_step s tr s' s'' __ x_18897
    1600     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18897)
     1596| Pft_step (s, tr, s', s'', x_2428) ->
     1597  h_pft_step s tr s' s'' __ x_2428
     1598    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428)
    16011599
    16021600(** val partial_flat_trace_rect_Type0 :
     
    16061604    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    16071605    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18902 x_18901 = function
     1606let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function
    16091607| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1610 | Pft_step (s, tr, s', s'', x_18905) ->
    1611   h_pft_step s tr s' s'' __ x_18905
    1612     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18905)
     1608| Pft_step (s, tr, s', s'', x_2436) ->
     1609  h_pft_step s tr s' s'' __ x_2436
     1610    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436)
    16131611
    16141612(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.