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/structuredTraces.ml

    r2775 r2797  
    219219    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    220220    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    221 let rec abstract_status_rect_Type4 h_mk_abstract_status x_16414 =
     221let rec abstract_status_rect_Type4 h_mk_abstract_status x_16427 =
    222222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    223223    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    224     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16414
     224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16427
    225225  in
    226226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    232232    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    233233    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    234 let rec abstract_status_rect_Type5 h_mk_abstract_status x_16416 =
     234let rec abstract_status_rect_Type5 h_mk_abstract_status x_16429 =
    235235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    236236    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    237     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16416
     237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16429
    238238  in
    239239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    245245    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    246246    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    247 let rec abstract_status_rect_Type3 h_mk_abstract_status x_16418 =
     247let rec abstract_status_rect_Type3 h_mk_abstract_status x_16431 =
    248248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    249249    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    250     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16418
     250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16431
    251251  in
    252252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    258258    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    259259    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    260 let rec abstract_status_rect_Type2 h_mk_abstract_status x_16420 =
     260let rec abstract_status_rect_Type2 h_mk_abstract_status x_16433 =
    261261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    262262    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    263     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16420
     263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16433
    264264  in
    265265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    271271    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    272272    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    273 let rec abstract_status_rect_Type1 h_mk_abstract_status x_16422 =
     273let rec abstract_status_rect_Type1 h_mk_abstract_status x_16435 =
    274274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    275275    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    276     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16422
     276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16435
    277277  in
    278278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    284284    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    285285    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    286 let rec abstract_status_rect_Type0 h_mk_abstract_status x_16424 =
     286let rec abstract_status_rect_Type0 h_mk_abstract_status x_16437 =
    287287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    288288    as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
    289     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16424
     289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16437
    290290  in
    291291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    821821    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    822822    __ -> trace_any_call -> 'a1 **)
    823 let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_16502 x_16501 = function
     823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_16515 x_16514 = function
    824824| Tac_base status -> h_tac_base status __
    825825| Tac_step_call
    826826    (status_pre_fun_call, status_after_fun_call, status_final,
    827      status_start_fun_call, x_16507, x_16505) ->
     827     status_start_fun_call, x_16520, x_16518) ->
    828828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    829     status_start_fun_call __ __ __ x_16507 __ x_16505
     829    status_start_fun_call __ __ __ x_16520 __ x_16518
    830830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    831       h_tac_step_default status_after_fun_call status_final x_16505)
    832 | Tac_step_default (status_pre, status_end, status_init, x_16512) ->
    833   h_tac_step_default status_pre status_end status_init __ x_16512 __ __
     831      h_tac_step_default status_after_fun_call status_final x_16518)
     832| Tac_step_default (status_pre, status_end, status_init, x_16525) ->
     833  h_tac_step_default status_pre status_end status_init __ x_16525 __ __
    834834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    835       h_tac_step_default status_init status_end x_16512)
     835      h_tac_step_default status_init status_end x_16525)
    836836
    837837(** val trace_any_call_rect_Type3 :
     
    840840    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    841841    __ -> trace_any_call -> 'a1 **)
    842 let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_16534 x_16533 = function
     842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_16547 x_16546 = function
    843843| Tac_base status -> h_tac_base status __
    844844| Tac_step_call
    845845    (status_pre_fun_call, status_after_fun_call, status_final,
    846      status_start_fun_call, x_16539, x_16537) ->
     846     status_start_fun_call, x_16552, x_16550) ->
    847847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    848     status_start_fun_call __ __ __ x_16539 __ x_16537
     848    status_start_fun_call __ __ __ x_16552 __ x_16550
    849849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    850       h_tac_step_default status_after_fun_call status_final x_16537)
    851 | Tac_step_default (status_pre, status_end, status_init, x_16544) ->
    852   h_tac_step_default status_pre status_end status_init __ x_16544 __ __
     850      h_tac_step_default status_after_fun_call status_final x_16550)
     851| Tac_step_default (status_pre, status_end, status_init, x_16557) ->
     852  h_tac_step_default status_pre status_end status_init __ x_16557 __ __
    853853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    854       h_tac_step_default status_init status_end x_16544)
     854      h_tac_step_default status_init status_end x_16557)
    855855
    856856(** val trace_any_call_rect_Type2 :
     
    859859    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    860860    __ -> trace_any_call -> 'a1 **)
    861 let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_16550 x_16549 = function
     861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_16563 x_16562 = function
    862862| Tac_base status -> h_tac_base status __
    863863| Tac_step_call
    864864    (status_pre_fun_call, status_after_fun_call, status_final,
    865      status_start_fun_call, x_16555, x_16553) ->
     865     status_start_fun_call, x_16568, x_16566) ->
    866866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    867     status_start_fun_call __ __ __ x_16555 __ x_16553
     867    status_start_fun_call __ __ __ x_16568 __ x_16566
    868868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    869       h_tac_step_default status_after_fun_call status_final x_16553)
    870 | Tac_step_default (status_pre, status_end, status_init, x_16560) ->
    871   h_tac_step_default status_pre status_end status_init __ x_16560 __ __
     869      h_tac_step_default status_after_fun_call status_final x_16566)
     870| Tac_step_default (status_pre, status_end, status_init, x_16573) ->
     871  h_tac_step_default status_pre status_end status_init __ x_16573 __ __
    872872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    873       h_tac_step_default status_init status_end x_16560)
     873      h_tac_step_default status_init status_end x_16573)
    874874
    875875(** val trace_any_call_rect_Type1 :
     
    878878    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    879879    __ -> trace_any_call -> 'a1 **)
    880 let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_16566 x_16565 = function
     880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_16579 x_16578 = function
    881881| Tac_base status -> h_tac_base status __
    882882| Tac_step_call
    883883    (status_pre_fun_call, status_after_fun_call, status_final,
    884      status_start_fun_call, x_16571, x_16569) ->
     884     status_start_fun_call, x_16584, x_16582) ->
    885885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    886     status_start_fun_call __ __ __ x_16571 __ x_16569
     886    status_start_fun_call __ __ __ x_16584 __ x_16582
    887887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    888       h_tac_step_default status_after_fun_call status_final x_16569)
    889 | Tac_step_default (status_pre, status_end, status_init, x_16576) ->
    890   h_tac_step_default status_pre status_end status_init __ x_16576 __ __
     888      h_tac_step_default status_after_fun_call status_final x_16582)
     889| Tac_step_default (status_pre, status_end, status_init, x_16589) ->
     890  h_tac_step_default status_pre status_end status_init __ x_16589 __ __
    891891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    892       h_tac_step_default status_init status_end x_16576)
     892      h_tac_step_default status_init status_end x_16589)
    893893
    894894(** val trace_any_call_rect_Type0 :
     
    897897    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    898898    __ -> trace_any_call -> 'a1 **)
    899 let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_16582 x_16581 = function
     899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_16595 x_16594 = function
    900900| Tac_base status -> h_tac_base status __
    901901| Tac_step_call
    902902    (status_pre_fun_call, status_after_fun_call, status_final,
    903      status_start_fun_call, x_16587, x_16585) ->
     903     status_start_fun_call, x_16600, x_16598) ->
    904904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    905     status_start_fun_call __ __ __ x_16587 __ x_16585
     905    status_start_fun_call __ __ __ x_16600 __ x_16598
    906906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    907       h_tac_step_default status_after_fun_call status_final x_16585)
    908 | Tac_step_default (status_pre, status_end, status_init, x_16592) ->
    909   h_tac_step_default status_pre status_end status_init __ x_16592 __ __
     907      h_tac_step_default status_after_fun_call status_final x_16598)
     908| Tac_step_default (status_pre, status_end, status_init, x_16605) ->
     909  h_tac_step_default status_pre status_end status_init __ x_16605 __ __
    910910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    911       h_tac_step_default status_init status_end x_16592)
     911      h_tac_step_default status_init status_end x_16605)
    912912
    913913(** val trace_any_call_inv_rect_Type4 :
     
    978978    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    979979    -> trace_label_call -> 'a1 **)
    980 let rec trace_label_call_rect_Type4 s h_tlc_base x_16700 x_16699 = function
    981 | Tlc_base (start_status, end_status, x_16703) ->
    982   h_tlc_base start_status end_status x_16703 __
     980let rec trace_label_call_rect_Type4 s h_tlc_base x_16713 x_16712 = function
     981| Tlc_base (start_status, end_status, x_16716) ->
     982  h_tlc_base start_status end_status x_16716 __
    983983
    984984(** val trace_label_call_rect_Type5 :
    985985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    986986    -> trace_label_call -> 'a1 **)
    987 let rec trace_label_call_rect_Type5 s h_tlc_base x_16706 x_16705 = function
    988 | Tlc_base (start_status, end_status, x_16709) ->
    989   h_tlc_base start_status end_status x_16709 __
     987let rec trace_label_call_rect_Type5 s h_tlc_base x_16719 x_16718 = function
     988| Tlc_base (start_status, end_status, x_16722) ->
     989  h_tlc_base start_status end_status x_16722 __
    990990
    991991(** val trace_label_call_rect_Type3 :
    992992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    993993    -> trace_label_call -> 'a1 **)
    994 let rec trace_label_call_rect_Type3 s h_tlc_base x_16712 x_16711 = function
    995 | Tlc_base (start_status, end_status, x_16715) ->
    996   h_tlc_base start_status end_status x_16715 __
     994let rec trace_label_call_rect_Type3 s h_tlc_base x_16725 x_16724 = function
     995| Tlc_base (start_status, end_status, x_16728) ->
     996  h_tlc_base start_status end_status x_16728 __
    997997
    998998(** val trace_label_call_rect_Type2 :
    999999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10001000    -> trace_label_call -> 'a1 **)
    1001 let rec trace_label_call_rect_Type2 s h_tlc_base x_16718 x_16717 = function
    1002 | Tlc_base (start_status, end_status, x_16721) ->
    1003   h_tlc_base start_status end_status x_16721 __
     1001let rec trace_label_call_rect_Type2 s h_tlc_base x_16731 x_16730 = function
     1002| Tlc_base (start_status, end_status, x_16734) ->
     1003  h_tlc_base start_status end_status x_16734 __
    10041004
    10051005(** val trace_label_call_rect_Type1 :
    10061006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10071007    -> trace_label_call -> 'a1 **)
    1008 let rec trace_label_call_rect_Type1 s h_tlc_base x_16724 x_16723 = function
    1009 | Tlc_base (start_status, end_status, x_16727) ->
    1010   h_tlc_base start_status end_status x_16727 __
     1008let rec trace_label_call_rect_Type1 s h_tlc_base x_16737 x_16736 = function
     1009| Tlc_base (start_status, end_status, x_16740) ->
     1010  h_tlc_base start_status end_status x_16740 __
    10111011
    10121012(** val trace_label_call_rect_Type0 :
    10131013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10141014    -> trace_label_call -> 'a1 **)
    1015 let rec trace_label_call_rect_Type0 s h_tlc_base x_16730 x_16729 = function
    1016 | Tlc_base (start_status, end_status, x_16733) ->
    1017   h_tlc_base start_status end_status x_16733 __
     1015let rec trace_label_call_rect_Type0 s h_tlc_base x_16743 x_16742 = function
     1016| Tlc_base (start_status, end_status, x_16746) ->
     1017  h_tlc_base start_status end_status x_16746 __
    10181018
    10191019(** val trace_label_call_inv_rect_Type4 :
     
    11701170    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11711171    -> trace_whole_program -> 'a1 **)
    1172 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_16782 = function
     1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_16795 = function
    11731173| Twp_terminating
    1174     (status_initial, status_start_fun, status_final, x_16785) ->
     1174    (status_initial, status_start_fun, status_final, x_16798) ->
    11751175  h_twp_terminating status_initial status_start_fun status_final __ __
    1176     x_16785 __
    1177 | Twp_diverges (status_initial, status_start_fun, x_16788) ->
    1178   h_twp_diverges status_initial status_start_fun __ __ x_16788
     1176    x_16798 __
     1177| Twp_diverges (status_initial, status_start_fun, x_16801) ->
     1178  h_twp_diverges status_initial status_start_fun __ __ x_16801
    11791179
    11801180(** val trace_whole_program_rect_Type5 :
     
    11821182    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11831183    -> trace_whole_program -> 'a1 **)
    1184 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_16793 = function
     1184let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_16806 = function
    11851185| Twp_terminating
    1186     (status_initial, status_start_fun, status_final, x_16796) ->
     1186    (status_initial, status_start_fun, status_final, x_16809) ->
    11871187  h_twp_terminating status_initial status_start_fun status_final __ __
    1188     x_16796 __
    1189 | Twp_diverges (status_initial, status_start_fun, x_16799) ->
    1190   h_twp_diverges status_initial status_start_fun __ __ x_16799
     1188    x_16809 __
     1189| Twp_diverges (status_initial, status_start_fun, x_16812) ->
     1190  h_twp_diverges status_initial status_start_fun __ __ x_16812
    11911191
    11921192(** val trace_whole_program_rect_Type3 :
     
    11941194    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11951195    -> trace_whole_program -> 'a1 **)
    1196 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_16804 = function
     1196let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_16817 = function
    11971197| Twp_terminating
    1198     (status_initial, status_start_fun, status_final, x_16807) ->
     1198    (status_initial, status_start_fun, status_final, x_16820) ->
    11991199  h_twp_terminating status_initial status_start_fun status_final __ __
    1200     x_16807 __
    1201 | Twp_diverges (status_initial, status_start_fun, x_16810) ->
    1202   h_twp_diverges status_initial status_start_fun __ __ x_16810
     1200    x_16820 __
     1201| Twp_diverges (status_initial, status_start_fun, x_16823) ->
     1202  h_twp_diverges status_initial status_start_fun __ __ x_16823
    12031203
    12041204(** val trace_whole_program_rect_Type2 :
     
    12061206    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12071207    -> trace_whole_program -> 'a1 **)
    1208 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_16815 = function
     1208let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_16828 = function
    12091209| Twp_terminating
    1210     (status_initial, status_start_fun, status_final, x_16818) ->
     1210    (status_initial, status_start_fun, status_final, x_16831) ->
    12111211  h_twp_terminating status_initial status_start_fun status_final __ __
    1212     x_16818 __
    1213 | Twp_diverges (status_initial, status_start_fun, x_16821) ->
    1214   h_twp_diverges status_initial status_start_fun __ __ x_16821
     1212    x_16831 __
     1213| Twp_diverges (status_initial, status_start_fun, x_16834) ->
     1214  h_twp_diverges status_initial status_start_fun __ __ x_16834
    12151215
    12161216(** val trace_whole_program_rect_Type1 :
     
    12181218    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12191219    -> trace_whole_program -> 'a1 **)
    1220 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_16826 = function
     1220let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_16839 = function
    12211221| Twp_terminating
    1222     (status_initial, status_start_fun, status_final, x_16829) ->
     1222    (status_initial, status_start_fun, status_final, x_16842) ->
    12231223  h_twp_terminating status_initial status_start_fun status_final __ __
    1224     x_16829 __
    1225 | Twp_diverges (status_initial, status_start_fun, x_16832) ->
    1226   h_twp_diverges status_initial status_start_fun __ __ x_16832
     1224    x_16842 __
     1225| Twp_diverges (status_initial, status_start_fun, x_16845) ->
     1226  h_twp_diverges status_initial status_start_fun __ __ x_16845
    12271227
    12281228(** val trace_whole_program_rect_Type0 :
     
    12301230    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12311231    -> trace_whole_program -> 'a1 **)
    1232 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_16837 = function
     1232let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_16850 = function
    12331233| Twp_terminating
    1234     (status_initial, status_start_fun, status_final, x_16840) ->
     1234    (status_initial, status_start_fun, status_final, x_16853) ->
    12351235  h_twp_terminating status_initial status_start_fun status_final __ __
    1236     x_16840 __
    1237 | Twp_diverges (status_initial, status_start_fun, x_16843) ->
    1238   h_twp_diverges status_initial status_start_fun __ __ x_16843
     1236    x_16853 __
     1237| Twp_diverges (status_initial, status_start_fun, x_16856) ->
     1238  h_twp_diverges status_initial status_start_fun __ __ x_16856
    12391239
    12401240(** val trace_whole_program_inv_rect_Type4 :
     
    13001300    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13011301    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1302 let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_17067 x_17066 = function
     1302let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_17080 x_17079 = function
    13031303| Taa_base st -> h_taa_base st
    1304 | Taa_step (st1, st2, st3, x_17069) ->
    1305   h_taa_step st1 st2 st3 __ __ __ x_17069
    1306     (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_17069)
     1304| Taa_step (st1, st2, st3, x_17082) ->
     1305  h_taa_step st1 st2 st3 __ __ __ x_17082
     1306    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_17082)
    13071307
    13081308(** val trace_any_any_rect_Type3 :
    13091309    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13101310    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1311 let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_17085 x_17084 = function
     1311let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_17098 x_17097 = function
    13121312| Taa_base st -> h_taa_base st
    1313 | Taa_step (st1, st2, st3, x_17087) ->
    1314   h_taa_step st1 st2 st3 __ __ __ x_17087
    1315     (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_17087)
     1313| Taa_step (st1, st2, st3, x_17100) ->
     1314  h_taa_step st1 st2 st3 __ __ __ x_17100
     1315    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_17100)
    13161316
    13171317(** val trace_any_any_rect_Type2 :
    13181318    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13191319    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1320 let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_17094 x_17093 = function
     1320let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_17107 x_17106 = function
    13211321| Taa_base st -> h_taa_base st
    1322 | Taa_step (st1, st2, st3, x_17096) ->
    1323   h_taa_step st1 st2 st3 __ __ __ x_17096
    1324     (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_17096)
     1322| Taa_step (st1, st2, st3, x_17109) ->
     1323  h_taa_step st1 st2 st3 __ __ __ x_17109
     1324    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_17109)
    13251325
    13261326(** val trace_any_any_rect_Type1 :
    13271327    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13281328    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1329 let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_17103 x_17102 = function
     1329let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_17116 x_17115 = function
    13301330| Taa_base st -> h_taa_base st
    1331 | Taa_step (st1, st2, st3, x_17105) ->
    1332   h_taa_step st1 st2 st3 __ __ __ x_17105
    1333     (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_17105)
     1331| Taa_step (st1, st2, st3, x_17118) ->
     1332  h_taa_step st1 st2 st3 __ __ __ x_17118
     1333    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_17118)
    13341334
    13351335(** val trace_any_any_rect_Type0 :
    13361336    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13371337    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1338 let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_17112 x_17111 = function
     1338let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_17125 x_17124 = function
    13391339| Taa_base st -> h_taa_base st
    1340 | Taa_step (st1, st2, st3, x_17114) ->
    1341   h_taa_step st1 st2 st3 __ __ __ x_17114
    1342     (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_17114)
     1340| Taa_step (st1, st2, st3, x_17127) ->
     1341  h_taa_step st1 st2 st3 __ __ __ x_17127
     1342    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_17127)
    13431343
    13441344(** val trace_any_any_inv_rect_Type4 :
     
    14561456    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14571457let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1458 | IEVcost x_17185 -> h_IEVcost x_17185
    1459 | IEVcall x_17186 -> h_IEVcall x_17186
    1460 | IEVtailcall (x_17188, x_17187) -> h_IEVtailcall x_17188 x_17187
    1461 | IEVret x_17189 -> h_IEVret x_17189
     1458| IEVcost x_17198 -> h_IEVcost x_17198
     1459| IEVcall x_17199 -> h_IEVcall x_17199
     1460| IEVtailcall (x_17201, x_17200) -> h_IEVtailcall x_17201 x_17200
     1461| IEVret x_17202 -> h_IEVret x_17202
    14621462
    14631463(** val intensional_event_rect_Type5 :
     
    14651465    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14661466let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1467 | IEVcost x_17195 -> h_IEVcost x_17195
    1468 | IEVcall x_17196 -> h_IEVcall x_17196
    1469 | IEVtailcall (x_17198, x_17197) -> h_IEVtailcall x_17198 x_17197
    1470 | IEVret x_17199 -> h_IEVret x_17199
     1467| IEVcost x_17208 -> h_IEVcost x_17208
     1468| IEVcall x_17209 -> h_IEVcall x_17209
     1469| IEVtailcall (x_17211, x_17210) -> h_IEVtailcall x_17211 x_17210
     1470| IEVret x_17212 -> h_IEVret x_17212
    14711471
    14721472(** val intensional_event_rect_Type3 :
     
    14741474    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14751475let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1476 | IEVcost x_17205 -> h_IEVcost x_17205
    1477 | IEVcall x_17206 -> h_IEVcall x_17206
    1478 | IEVtailcall (x_17208, x_17207) -> h_IEVtailcall x_17208 x_17207
    1479 | IEVret x_17209 -> h_IEVret x_17209
     1476| IEVcost x_17218 -> h_IEVcost x_17218
     1477| IEVcall x_17219 -> h_IEVcall x_17219
     1478| IEVtailcall (x_17221, x_17220) -> h_IEVtailcall x_17221 x_17220
     1479| IEVret x_17222 -> h_IEVret x_17222
    14801480
    14811481(** val intensional_event_rect_Type2 :
     
    14831483    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14841484let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1485 | IEVcost x_17215 -> h_IEVcost x_17215
    1486 | IEVcall x_17216 -> h_IEVcall x_17216
    1487 | IEVtailcall (x_17218, x_17217) -> h_IEVtailcall x_17218 x_17217
    1488 | IEVret x_17219 -> h_IEVret x_17219
     1485| IEVcost x_17228 -> h_IEVcost x_17228
     1486| IEVcall x_17229 -> h_IEVcall x_17229
     1487| IEVtailcall (x_17231, x_17230) -> h_IEVtailcall x_17231 x_17230
     1488| IEVret x_17232 -> h_IEVret x_17232
    14891489
    14901490(** val intensional_event_rect_Type1 :
     
    14921492    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14931493let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1494 | IEVcost x_17225 -> h_IEVcost x_17225
    1495 | IEVcall x_17226 -> h_IEVcall x_17226
    1496 | IEVtailcall (x_17228, x_17227) -> h_IEVtailcall x_17228 x_17227
    1497 | IEVret x_17229 -> h_IEVret x_17229
     1494| IEVcost x_17238 -> h_IEVcost x_17238
     1495| IEVcall x_17239 -> h_IEVcall x_17239
     1496| IEVtailcall (x_17241, x_17240) -> h_IEVtailcall x_17241 x_17240
     1497| IEVret x_17242 -> h_IEVret x_17242
    14981498
    14991499(** val intensional_event_rect_Type0 :
     
    15011501    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    15021502let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
    1503 | IEVcost x_17235 -> h_IEVcost x_17235
    1504 | IEVcall x_17236 -> h_IEVcall x_17236
    1505 | IEVtailcall (x_17238, x_17237) -> h_IEVtailcall x_17238 x_17237
    1506 | IEVret x_17239 -> h_IEVret x_17239
     1503| IEVcost x_17248 -> h_IEVcost x_17248
     1504| IEVcall x_17249 -> h_IEVcall x_17249
     1505| IEVtailcall (x_17251, x_17250) -> h_IEVtailcall x_17251 x_17250
     1506| IEVret x_17252 -> h_IEVret x_17252
    15071507
    15081508(** val intensional_event_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.