Changeset 2797 for extracted/csem.ml
 Timestamp:
 Mar 7, 2013, 12:55:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/csem.ml
r2775 r2797 778 778 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 779 779  Kstop > h_Kstop 780  Kseq (x_85 57, x_8556) >781 h_Kseq x_85 57 x_8556780  Kseq (x_8570, x_8569) > 781 h_Kseq x_8570 x_8569 782 782 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 783 h_Kswitch h_Kcall x_85 56)784  Kwhile (x_85 60, x_8559, x_8558) >785 h_Kwhile x_85 60 x_8559 x_8558783 h_Kswitch h_Kcall x_8569) 784  Kwhile (x_8573, x_8572, x_8571) > 785 h_Kwhile x_8573 x_8572 x_8571 786 786 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 787 h_Kswitch h_Kcall x_85 58)788  Kdowhile (x_85 63, x_8562, x_8561) >789 h_Kdowhile x_85 63 x_8562 x_8561787 h_Kswitch h_Kcall x_8571) 788  Kdowhile (x_8576, x_8575, x_8574) > 789 h_Kdowhile x_8576 x_8575 x_8574 790 790 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 791 h_Kswitch h_Kcall x_85 61)792  Kfor2 (x_85 67, x_8566, x_8565, x_8564) >793 h_Kfor2 x_85 67 x_8566 x_8565 x_8564791 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 794 794 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 795 h_Kswitch h_Kcall x_85 64)796  Kfor3 (x_85 71, x_8570, x_8569, x_8568) >797 h_Kfor3 x_85 71 x_8570 x_8569 x_8568795 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 798 798 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 799 h_Kswitch h_Kcall x_85 68)800  Kswitch x_85 72>801 h_Kswitch x_85 72799 h_Kswitch h_Kcall x_8581) 800  Kswitch x_8585 > 801 h_Kswitch x_8585 802 802 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 803 h_Kswitch h_Kcall x_85 72)804  Kcall (x_85 76, x_8575, x_8574, x_8573) >805 h_Kcall x_85 76 x_8575 x_8574 x_8573803 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 806 806 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 807 h_Kswitch h_Kcall x_85 73)807 h_Kswitch h_Kcall x_8586) 808 808 809 809 (** val cont_rect_Type3 : … … 818 818 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 819 819  Kstop > h_Kstop 820  Kseq (x_86 17, x_8616) >821 h_Kseq x_86 17 x_8616820  Kseq (x_8630, x_8629) > 821 h_Kseq x_8630 x_8629 822 822 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 823 h_Kswitch h_Kcall x_86 16)824  Kwhile (x_86 20, x_8619, x_8618) >825 h_Kwhile x_86 20 x_8619 x_8618823 h_Kswitch h_Kcall x_8629) 824  Kwhile (x_8633, x_8632, x_8631) > 825 h_Kwhile x_8633 x_8632 x_8631 826 826 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 827 h_Kswitch h_Kcall x_86 18)828  Kdowhile (x_86 23, x_8622, x_8621) >829 h_Kdowhile x_86 23 x_8622 x_8621827 h_Kswitch h_Kcall x_8631) 828  Kdowhile (x_8636, x_8635, x_8634) > 829 h_Kdowhile x_8636 x_8635 x_8634 830 830 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 831 h_Kswitch h_Kcall x_86 21)832  Kfor2 (x_86 27, x_8626, x_8625, x_8624) >833 h_Kfor2 x_86 27 x_8626 x_8625 x_8624831 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 834 834 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 835 h_Kswitch h_Kcall x_86 24)836  Kfor3 (x_86 31, x_8630, x_8629, x_8628) >837 h_Kfor3 x_86 31 x_8630 x_8629 x_8628835 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 838 838 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 839 h_Kswitch h_Kcall x_86 28)840  Kswitch x_86 32>841 h_Kswitch x_86 32839 h_Kswitch h_Kcall x_8641) 840  Kswitch x_8645 > 841 h_Kswitch x_8645 842 842 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 843 h_Kswitch h_Kcall x_86 32)844  Kcall (x_86 36, x_8635, x_8634, x_8633) >845 h_Kcall x_86 36 x_8635 x_8634 x_8633843 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 846 846 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 847 h_Kswitch h_Kcall x_86 33)847 h_Kswitch h_Kcall x_8646) 848 848 849 849 (** val cont_rect_Type2 : … … 858 858 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 859 859  Kstop > h_Kstop 860  Kseq (x_86 47, x_8646) >861 h_Kseq x_86 47 x_8646860  Kseq (x_8660, x_8659) > 861 h_Kseq x_8660 x_8659 862 862 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 863 h_Kswitch h_Kcall x_86 46)864  Kwhile (x_86 50, x_8649, x_8648) >865 h_Kwhile x_86 50 x_8649 x_8648863 h_Kswitch h_Kcall x_8659) 864  Kwhile (x_8663, x_8662, x_8661) > 865 h_Kwhile x_8663 x_8662 x_8661 866 866 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 867 h_Kswitch h_Kcall x_86 48)868  Kdowhile (x_86 53, x_8652, x_8651) >869 h_Kdowhile x_86 53 x_8652 x_8651867 h_Kswitch h_Kcall x_8661) 868  Kdowhile (x_8666, x_8665, x_8664) > 869 h_Kdowhile x_8666 x_8665 x_8664 870 870 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 871 h_Kswitch h_Kcall x_86 51)872  Kfor2 (x_86 57, x_8656, x_8655, x_8654) >873 h_Kfor2 x_86 57 x_8656 x_8655 x_8654871 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 874 874 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 875 h_Kswitch h_Kcall x_86 54)876  Kfor3 (x_86 61, x_8660, x_8659, x_8658) >877 h_Kfor3 x_86 61 x_8660 x_8659 x_8658875 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 878 878 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 879 h_Kswitch h_Kcall x_86 58)880  Kswitch x_86 62>881 h_Kswitch x_86 62879 h_Kswitch h_Kcall x_8671) 880  Kswitch x_8675 > 881 h_Kswitch x_8675 882 882 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 883 h_Kswitch h_Kcall x_86 62)884  Kcall (x_86 66, x_8665, x_8664, x_8663) >885 h_Kcall x_86 66 x_8665 x_8664 x_8663883 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 886 886 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 887 h_Kswitch h_Kcall x_86 63)887 h_Kswitch h_Kcall x_8676) 888 888 889 889 (** val cont_rect_Type1 : … … 898 898 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 899 899  Kstop > h_Kstop 900  Kseq (x_86 77, x_8676) >901 h_Kseq x_86 77 x_8676900  Kseq (x_8690, x_8689) > 901 h_Kseq x_8690 x_8689 902 902 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 903 h_Kswitch h_Kcall x_86 76)904  Kwhile (x_86 80, x_8679, x_8678) >905 h_Kwhile x_86 80 x_8679 x_8678903 h_Kswitch h_Kcall x_8689) 904  Kwhile (x_8693, x_8692, x_8691) > 905 h_Kwhile x_8693 x_8692 x_8691 906 906 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 907 h_Kswitch h_Kcall x_86 78)908  Kdowhile (x_86 83, x_8682, x_8681) >909 h_Kdowhile x_86 83 x_8682 x_8681907 h_Kswitch h_Kcall x_8691) 908  Kdowhile (x_8696, x_8695, x_8694) > 909 h_Kdowhile x_8696 x_8695 x_8694 910 910 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 911 h_Kswitch h_Kcall x_86 81)912  Kfor2 (x_8 687, x_8686, x_8685, x_8684) >913 h_Kfor2 x_8 687 x_8686 x_8685 x_8684911 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 914 914 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 915 h_Kswitch h_Kcall x_86 84)916  Kfor3 (x_8 691, x_8690, x_8689, x_8688) >917 h_Kfor3 x_8 691 x_8690 x_8689 x_8688915 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 918 918 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 919 h_Kswitch h_Kcall x_8 688)920  Kswitch x_8 692>921 h_Kswitch x_8 692919 h_Kswitch h_Kcall x_8701) 920  Kswitch x_8705 > 921 h_Kswitch x_8705 922 922 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 923 h_Kswitch h_Kcall x_8 692)924  Kcall (x_8 696, x_8695, x_8694, x_8693) >925 h_Kcall x_8 696 x_8695 x_8694 x_8693923 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 926 926 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 927 h_Kswitch h_Kcall x_8 693)927 h_Kswitch h_Kcall x_8706) 928 928 929 929 (** val cont_rect_Type0 : … … 938 938 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 939 939  Kstop > h_Kstop 940  Kseq (x_87 07, x_8706) >941 h_Kseq x_87 07 x_8706940  Kseq (x_8720, x_8719) > 941 h_Kseq x_8720 x_8719 942 942 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 943 h_Kswitch h_Kcall x_87 06)944  Kwhile (x_87 10, x_8709, x_8708) >945 h_Kwhile x_87 10 x_8709 x_8708943 h_Kswitch h_Kcall x_8719) 944  Kwhile (x_8723, x_8722, x_8721) > 945 h_Kwhile x_8723 x_8722 x_8721 946 946 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 947 h_Kswitch h_Kcall x_87 08)948  Kdowhile (x_87 13, x_8712, x_8711) >949 h_Kdowhile x_87 13 x_8712 x_8711947 h_Kswitch h_Kcall x_8721) 948  Kdowhile (x_8726, x_8725, x_8724) > 949 h_Kdowhile x_8726 x_8725 x_8724 950 950 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 951 h_Kswitch h_Kcall x_87 11)952  Kfor2 (x_87 17, x_8716, x_8715, x_8714) >953 h_Kfor2 x_87 17 x_8716 x_8715 x_8714951 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 954 954 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 955 h_Kswitch h_Kcall x_87 14)956  Kfor3 (x_87 21, x_8720, x_8719, x_8718) >957 h_Kfor3 x_87 21 x_8720 x_8719 x_8718955 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 958 958 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 959 h_Kswitch h_Kcall x_87 18)960  Kswitch x_87 22>961 h_Kswitch x_87 22959 h_Kswitch h_Kcall x_8731) 960  Kswitch x_8735 > 961 h_Kswitch x_8735 962 962 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 963 h_Kswitch h_Kcall x_87 22)964  Kcall (x_87 26, x_8725, x_8724, x_8723) >965 h_Kcall x_87 26 x_8725 x_8724 x_8723963 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 966 966 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 967 h_Kswitch h_Kcall x_87 23)967 h_Kswitch h_Kcall x_8736) 968 968 969 969 (** val cont_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.