Changeset 2827 for extracted/csem.ml


Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (8 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.ml

    r2797 r2827  
    778778let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    779779| Kstop -> h_Kstop
    780 | Kseq (x_8570, x_8569) ->
    781   h_Kseq x_8570 x_8569
     780| Kseq (x_8687, x_8686) ->
     781  h_Kseq x_8687 x_8686
    782782    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    783       h_Kswitch h_Kcall x_8569)
    784 | Kwhile (x_8573, x_8572, x_8571) ->
    785   h_Kwhile x_8573 x_8572 x_8571
     783      h_Kswitch h_Kcall x_8686)
     784| Kwhile (x_8690, x_8689, x_8688) ->
     785  h_Kwhile x_8690 x_8689 x_8688
    786786    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    787       h_Kswitch h_Kcall x_8571)
    788 | Kdowhile (x_8576, x_8575, x_8574) ->
    789   h_Kdowhile x_8576 x_8575 x_8574
     787      h_Kswitch h_Kcall x_8688)
     788| Kdowhile (x_8693, x_8692, x_8691) ->
     789  h_Kdowhile x_8693 x_8692 x_8691
    790790    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    791       h_Kswitch h_Kcall x_8574)
    792 | Kfor2 (x_8580, x_8579, x_8578, x_8577) ->
    793   h_Kfor2 x_8580 x_8579 x_8578 x_8577
     791      h_Kswitch h_Kcall x_8691)
     792| Kfor2 (x_8697, x_8696, x_8695, x_8694) ->
     793  h_Kfor2 x_8697 x_8696 x_8695 x_8694
    794794    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    795       h_Kswitch h_Kcall x_8577)
    796 | Kfor3 (x_8584, x_8583, x_8582, x_8581) ->
    797   h_Kfor3 x_8584 x_8583 x_8582 x_8581
     795      h_Kswitch h_Kcall x_8694)
     796| Kfor3 (x_8701, x_8700, x_8699, x_8698) ->
     797  h_Kfor3 x_8701 x_8700 x_8699 x_8698
    798798    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    799       h_Kswitch h_Kcall x_8581)
    800 | Kswitch x_8585 ->
    801   h_Kswitch x_8585
     799      h_Kswitch h_Kcall x_8698)
     800| Kswitch x_8702 ->
     801  h_Kswitch x_8702
    802802    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    803       h_Kswitch h_Kcall x_8585)
    804 | Kcall (x_8589, x_8588, x_8587, x_8586) ->
    805   h_Kcall x_8589 x_8588 x_8587 x_8586
     803      h_Kswitch h_Kcall x_8702)
     804| Kcall (x_8706, x_8705, x_8704, x_8703) ->
     805  h_Kcall x_8706 x_8705 x_8704 x_8703
    806806    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    807       h_Kswitch h_Kcall x_8586)
     807      h_Kswitch h_Kcall x_8703)
    808808
    809809(** val cont_rect_Type3 :
     
    818818let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    819819| Kstop -> h_Kstop
    820 | Kseq (x_8630, x_8629) ->
    821   h_Kseq x_8630 x_8629
     820| Kseq (x_8747, x_8746) ->
     821  h_Kseq x_8747 x_8746
    822822    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    823       h_Kswitch h_Kcall x_8629)
    824 | Kwhile (x_8633, x_8632, x_8631) ->
    825   h_Kwhile x_8633 x_8632 x_8631
     823      h_Kswitch h_Kcall x_8746)
     824| Kwhile (x_8750, x_8749, x_8748) ->
     825  h_Kwhile x_8750 x_8749 x_8748
    826826    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    827       h_Kswitch h_Kcall x_8631)
    828 | Kdowhile (x_8636, x_8635, x_8634) ->
    829   h_Kdowhile x_8636 x_8635 x_8634
     827      h_Kswitch h_Kcall x_8748)
     828| Kdowhile (x_8753, x_8752, x_8751) ->
     829  h_Kdowhile x_8753 x_8752 x_8751
    830830    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    831       h_Kswitch h_Kcall x_8634)
    832 | Kfor2 (x_8640, x_8639, x_8638, x_8637) ->
    833   h_Kfor2 x_8640 x_8639 x_8638 x_8637
     831      h_Kswitch h_Kcall x_8751)
     832| Kfor2 (x_8757, x_8756, x_8755, x_8754) ->
     833  h_Kfor2 x_8757 x_8756 x_8755 x_8754
    834834    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    835       h_Kswitch h_Kcall x_8637)
    836 | Kfor3 (x_8644, x_8643, x_8642, x_8641) ->
    837   h_Kfor3 x_8644 x_8643 x_8642 x_8641
     835      h_Kswitch h_Kcall x_8754)
     836| Kfor3 (x_8761, x_8760, x_8759, x_8758) ->
     837  h_Kfor3 x_8761 x_8760 x_8759 x_8758
    838838    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    839       h_Kswitch h_Kcall x_8641)
    840 | Kswitch x_8645 ->
    841   h_Kswitch x_8645
     839      h_Kswitch h_Kcall x_8758)
     840| Kswitch x_8762 ->
     841  h_Kswitch x_8762
    842842    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    843       h_Kswitch h_Kcall x_8645)
    844 | Kcall (x_8649, x_8648, x_8647, x_8646) ->
    845   h_Kcall x_8649 x_8648 x_8647 x_8646
     843      h_Kswitch h_Kcall x_8762)
     844| Kcall (x_8766, x_8765, x_8764, x_8763) ->
     845  h_Kcall x_8766 x_8765 x_8764 x_8763
    846846    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    847       h_Kswitch h_Kcall x_8646)
     847      h_Kswitch h_Kcall x_8763)
    848848
    849849(** val cont_rect_Type2 :
     
    858858let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    859859| Kstop -> h_Kstop
    860 | Kseq (x_8660, x_8659) ->
    861   h_Kseq x_8660 x_8659
     860| Kseq (x_8777, x_8776) ->
     861  h_Kseq x_8777 x_8776
    862862    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    863       h_Kswitch h_Kcall x_8659)
    864 | Kwhile (x_8663, x_8662, x_8661) ->
    865   h_Kwhile x_8663 x_8662 x_8661
     863      h_Kswitch h_Kcall x_8776)
     864| Kwhile (x_8780, x_8779, x_8778) ->
     865  h_Kwhile x_8780 x_8779 x_8778
    866866    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    867       h_Kswitch h_Kcall x_8661)
    868 | Kdowhile (x_8666, x_8665, x_8664) ->
    869   h_Kdowhile x_8666 x_8665 x_8664
     867      h_Kswitch h_Kcall x_8778)
     868| Kdowhile (x_8783, x_8782, x_8781) ->
     869  h_Kdowhile x_8783 x_8782 x_8781
    870870    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    871       h_Kswitch h_Kcall x_8664)
    872 | Kfor2 (x_8670, x_8669, x_8668, x_8667) ->
    873   h_Kfor2 x_8670 x_8669 x_8668 x_8667
     871      h_Kswitch h_Kcall x_8781)
     872| Kfor2 (x_8787, x_8786, x_8785, x_8784) ->
     873  h_Kfor2 x_8787 x_8786 x_8785 x_8784
    874874    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    875       h_Kswitch h_Kcall x_8667)
    876 | Kfor3 (x_8674, x_8673, x_8672, x_8671) ->
    877   h_Kfor3 x_8674 x_8673 x_8672 x_8671
     875      h_Kswitch h_Kcall x_8784)
     876| Kfor3 (x_8791, x_8790, x_8789, x_8788) ->
     877  h_Kfor3 x_8791 x_8790 x_8789 x_8788
    878878    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    879       h_Kswitch h_Kcall x_8671)
    880 | Kswitch x_8675 ->
    881   h_Kswitch x_8675
     879      h_Kswitch h_Kcall x_8788)
     880| Kswitch x_8792 ->
     881  h_Kswitch x_8792
    882882    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    883       h_Kswitch h_Kcall x_8675)
    884 | Kcall (x_8679, x_8678, x_8677, x_8676) ->
    885   h_Kcall x_8679 x_8678 x_8677 x_8676
     883      h_Kswitch h_Kcall x_8792)
     884| Kcall (x_8796, x_8795, x_8794, x_8793) ->
     885  h_Kcall x_8796 x_8795 x_8794 x_8793
    886886    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    887       h_Kswitch h_Kcall x_8676)
     887      h_Kswitch h_Kcall x_8793)
    888888
    889889(** val cont_rect_Type1 :
     
    898898let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    899899| Kstop -> h_Kstop
    900 | Kseq (x_8690, x_8689) ->
    901   h_Kseq x_8690 x_8689
     900| Kseq (x_8807, x_8806) ->
     901  h_Kseq x_8807 x_8806
    902902    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    903       h_Kswitch h_Kcall x_8689)
    904 | Kwhile (x_8693, x_8692, x_8691) ->
    905   h_Kwhile x_8693 x_8692 x_8691
     903      h_Kswitch h_Kcall x_8806)
     904| Kwhile (x_8810, x_8809, x_8808) ->
     905  h_Kwhile x_8810 x_8809 x_8808
    906906    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    907       h_Kswitch h_Kcall x_8691)
    908 | Kdowhile (x_8696, x_8695, x_8694) ->
    909   h_Kdowhile x_8696 x_8695 x_8694
     907      h_Kswitch h_Kcall x_8808)
     908| Kdowhile (x_8813, x_8812, x_8811) ->
     909  h_Kdowhile x_8813 x_8812 x_8811
    910910    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    911       h_Kswitch h_Kcall x_8694)
    912 | Kfor2 (x_8700, x_8699, x_8698, x_8697) ->
    913   h_Kfor2 x_8700 x_8699 x_8698 x_8697
     911      h_Kswitch h_Kcall x_8811)
     912| Kfor2 (x_8817, x_8816, x_8815, x_8814) ->
     913  h_Kfor2 x_8817 x_8816 x_8815 x_8814
    914914    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    915       h_Kswitch h_Kcall x_8697)
    916 | Kfor3 (x_8704, x_8703, x_8702, x_8701) ->
    917   h_Kfor3 x_8704 x_8703 x_8702 x_8701
     915      h_Kswitch h_Kcall x_8814)
     916| Kfor3 (x_8821, x_8820, x_8819, x_8818) ->
     917  h_Kfor3 x_8821 x_8820 x_8819 x_8818
    918918    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    919       h_Kswitch h_Kcall x_8701)
    920 | Kswitch x_8705 ->
    921   h_Kswitch x_8705
     919      h_Kswitch h_Kcall x_8818)
     920| Kswitch x_8822 ->
     921  h_Kswitch x_8822
    922922    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    923       h_Kswitch h_Kcall x_8705)
    924 | Kcall (x_8709, x_8708, x_8707, x_8706) ->
    925   h_Kcall x_8709 x_8708 x_8707 x_8706
     923      h_Kswitch h_Kcall x_8822)
     924| Kcall (x_8826, x_8825, x_8824, x_8823) ->
     925  h_Kcall x_8826 x_8825 x_8824 x_8823
    926926    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    927       h_Kswitch h_Kcall x_8706)
     927      h_Kswitch h_Kcall x_8823)
    928928
    929929(** val cont_rect_Type0 :
     
    938938let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
    939939| Kstop -> h_Kstop
    940 | Kseq (x_8720, x_8719) ->
    941   h_Kseq x_8720 x_8719
     940| Kseq (x_8837, x_8836) ->
     941  h_Kseq x_8837 x_8836
    942942    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    943       h_Kswitch h_Kcall x_8719)
    944 | Kwhile (x_8723, x_8722, x_8721) ->
    945   h_Kwhile x_8723 x_8722 x_8721
     943      h_Kswitch h_Kcall x_8836)
     944| Kwhile (x_8840, x_8839, x_8838) ->
     945  h_Kwhile x_8840 x_8839 x_8838
    946946    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    947       h_Kswitch h_Kcall x_8721)
    948 | Kdowhile (x_8726, x_8725, x_8724) ->
    949   h_Kdowhile x_8726 x_8725 x_8724
     947      h_Kswitch h_Kcall x_8838)
     948| Kdowhile (x_8843, x_8842, x_8841) ->
     949  h_Kdowhile x_8843 x_8842 x_8841
    950950    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    951       h_Kswitch h_Kcall x_8724)
    952 | Kfor2 (x_8730, x_8729, x_8728, x_8727) ->
    953   h_Kfor2 x_8730 x_8729 x_8728 x_8727
     951      h_Kswitch h_Kcall x_8841)
     952| Kfor2 (x_8847, x_8846, x_8845, x_8844) ->
     953  h_Kfor2 x_8847 x_8846 x_8845 x_8844
    954954    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    955       h_Kswitch h_Kcall x_8727)
    956 | Kfor3 (x_8734, x_8733, x_8732, x_8731) ->
    957   h_Kfor3 x_8734 x_8733 x_8732 x_8731
     955      h_Kswitch h_Kcall x_8844)
     956| Kfor3 (x_8851, x_8850, x_8849, x_8848) ->
     957  h_Kfor3 x_8851 x_8850 x_8849 x_8848
    958958    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    959       h_Kswitch h_Kcall x_8731)
    960 | Kswitch x_8735 ->
    961   h_Kswitch x_8735
     959      h_Kswitch h_Kcall x_8848)
     960| Kswitch x_8852 ->
     961  h_Kswitch x_8852
    962962    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    963       h_Kswitch h_Kcall x_8735)
    964 | Kcall (x_8739, x_8738, x_8737, x_8736) ->
    965   h_Kcall x_8739 x_8738 x_8737 x_8736
     963      h_Kswitch h_Kcall x_8852)
     964| Kcall (x_8856, x_8855, x_8854, x_8853) ->
     965  h_Kcall x_8856 x_8855 x_8854 x_8853
    966966    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
    967       h_Kswitch h_Kcall x_8736)
     967      h_Kswitch h_Kcall x_8853)
    968968
    969969(** val cont_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.