Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.ml

    r2775 r2797  
    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_17579 s x_17578 = function
    299 | Wr_step (s0, tr, s', depth, trace, x_17581) ->
    300   h_wr_step s0 tr s' depth __ trace __ x_17581
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17592 s x_17591 = function
     299| Wr_step (s0, tr, s', depth, trace, x_17594) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_17594
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    302       s' trace x_17581)
    303 | Wr_call (s0, tr, s', depth, trace, x_17583) ->
    304   h_wr_call s0 tr s' depth __ trace __ x_17583
     302      s' trace x_17594)
     303| Wr_call (s0, tr, s', depth, trace, x_17596) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_17596
    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_17583)
    307 | Wr_ret (s0, tr, s', depth, trace, x_17585) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_17585
     306      depth) s' trace x_17596)
     307| Wr_ret (s0, tr, s', depth, trace, x_17598) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_17598
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_17585)
     310      s' trace x_17598)
    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_17607 s x_17606 = function
    326 | Wr_step (s0, tr, s', depth, trace, x_17609) ->
    327   h_wr_step s0 tr s' depth __ trace __ x_17609
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17620 s x_17619 = function
     326| Wr_step (s0, tr, s', depth, trace, x_17622) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_17622
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    329       s' trace x_17609)
    330 | Wr_call (s0, tr, s', depth, trace, x_17611) ->
    331   h_wr_call s0 tr s' depth __ trace __ x_17611
     329      s' trace x_17622)
     330| Wr_call (s0, tr, s', depth, trace, x_17624) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_17624
    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_17611)
    334 | Wr_ret (s0, tr, s', depth, trace, x_17613) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_17613
     333      depth) s' trace x_17624)
     334| Wr_ret (s0, tr, s', depth, trace, x_17626) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_17626
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_17613)
     337      s' trace x_17626)
    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_17621 s x_17620 = function
    353 | Wr_step (s0, tr, s', depth, trace, x_17623) ->
    354   h_wr_step s0 tr s' depth __ trace __ x_17623
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17634 s x_17633 = function
     353| Wr_step (s0, tr, s', depth, trace, x_17636) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_17636
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    356       s' trace x_17623)
    357 | Wr_call (s0, tr, s', depth, trace, x_17625) ->
    358   h_wr_call s0 tr s' depth __ trace __ x_17625
     356      s' trace x_17636)
     357| Wr_call (s0, tr, s', depth, trace, x_17638) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_17638
    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_17625)
    361 | Wr_ret (s0, tr, s', depth, trace, x_17627) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_17627
     360      depth) s' trace x_17638)
     361| Wr_ret (s0, tr, s', depth, trace, x_17640) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_17640
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_17627)
     364      s' trace x_17640)
    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_17635 s x_17634 = function
    380 | Wr_step (s0, tr, s', depth, trace, x_17637) ->
    381   h_wr_step s0 tr s' depth __ trace __ x_17637
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17648 s x_17647 = function
     380| Wr_step (s0, tr, s', depth, trace, x_17650) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_17650
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    383       s' trace x_17637)
    384 | Wr_call (s0, tr, s', depth, trace, x_17639) ->
    385   h_wr_call s0 tr s' depth __ trace __ x_17639
     383      s' trace x_17650)
     384| Wr_call (s0, tr, s', depth, trace, x_17652) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_17652
    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_17639)
    388 | Wr_ret (s0, tr, s', depth, trace, x_17641) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_17641
     387      depth) s' trace x_17652)
     388| Wr_ret (s0, tr, s', depth, trace, x_17654) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_17654
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_17641)
     391      s' trace x_17654)
    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_17649 s x_17648 = function
    407 | Wr_step (s0, tr, s', depth, trace, x_17651) ->
    408   h_wr_step s0 tr s' depth __ trace __ x_17651
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17662 s x_17661 = function
     407| Wr_step (s0, tr, s', depth, trace, x_17664) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_17664
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    410       s' trace x_17651)
    411 | Wr_call (s0, tr, s', depth, trace, x_17653) ->
    412   h_wr_call s0 tr s' depth __ trace __ x_17653
     410      s' trace x_17664)
     411| Wr_call (s0, tr, s', depth, trace, x_17666) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_17666
    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_17653)
    415 | Wr_ret (s0, tr, s', depth, trace, x_17655) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_17655
     414      depth) s' trace x_17666)
     415| Wr_ret (s0, tr, s', depth, trace, x_17668) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_17668
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_17655)
     418      s' trace x_17668)
    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_18190 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18203 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_18190
     843    new_trace0; terminates = terminates0 } = x_18203
    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_18192 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18205 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18192
     855    new_trace0; terminates = terminates0 } = x_18205
    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_18194 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18207 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18194
     867    new_trace0; terminates = terminates0 } = x_18207
    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_18196 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18209 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18196
     879    new_trace0; terminates = terminates0 } = x_18209
    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_18198 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18211 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18198
     891    new_trace0; terminates = terminates0 } = x_18211
    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_18200 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18213 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18200
     903    new_trace0; terminates = terminates0 } = x_18213
    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_18218 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_18218 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18231 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_18231 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_18220 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_18220 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18233 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_18233 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_18222 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_18222 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18235 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_18235 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_18224 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_18224 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18237 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_18237 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_18226 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_18226 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18239 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_18239 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_18228 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_18228 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18241 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_18241 in
    10481048  h_mk_sub_trace_result ends0 trace_res0
    10491049
     
    15581558    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15591559    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_18563 x_18562 = function
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18576 x_18575 = function
    15611561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1562 | Pft_step (s, tr, s', s'', x_18566) ->
    1563   h_pft_step s tr s' s'' __ x_18566
    1564     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18566)
     1562| Pft_step (s, tr, s', s'', x_18579) ->
     1563  h_pft_step s tr s' s'' __ x_18579
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18579)
    15651565
    15661566(** val partial_flat_trace_rect_Type3 :
     
    15701570    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15711571    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_18579 x_18578 = function
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18592 x_18591 = function
    15731573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1574 | Pft_step (s, tr, s', s'', x_18582) ->
    1575   h_pft_step s tr s' s'' __ x_18582
    1576     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18582)
     1574| Pft_step (s, tr, s', s'', x_18595) ->
     1575  h_pft_step s tr s' s'' __ x_18595
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18595)
    15771577
    15781578(** val partial_flat_trace_rect_Type2 :
     
    15821582    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15831583    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_18587 x_18586 = function
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18600 x_18599 = function
    15851585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1586 | Pft_step (s, tr, s', s'', x_18590) ->
    1587   h_pft_step s tr s' s'' __ x_18590
    1588     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18590)
     1586| Pft_step (s, tr, s', s'', x_18603) ->
     1587  h_pft_step s tr s' s'' __ x_18603
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18603)
    15891589
    15901590(** val partial_flat_trace_rect_Type1 :
     
    15941594    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15951595    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_18595 x_18594 = function
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18608 x_18607 = function
    15971597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1598 | Pft_step (s, tr, s', s'', x_18598) ->
    1599   h_pft_step s tr s' s'' __ x_18598
    1600     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18598)
     1598| Pft_step (s, tr, s', s'', x_18611) ->
     1599  h_pft_step s tr s' s'' __ x_18611
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18611)
    16011601
    16021602(** val partial_flat_trace_rect_Type0 :
     
    16061606    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    16071607    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_18603 x_18602 = function
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18616 x_18615 = function
    16091609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1610 | Pft_step (s, tr, s', s'', x_18606) ->
    1611   h_pft_step s tr s' s'' __ x_18606
    1612     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18606)
     1610| Pft_step (s, tr, s', s'', x_18619) ->
     1611  h_pft_step s tr s' s'' __ x_18619
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18619)
    16131613
    16141614(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.