Changeset 2717 for extracted/csem.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/csem.ml
r2649 r2717 37 37 open Identifiers 38 38 39 open Exp 40 39 41 open Arithmetic 40 42 … … 92 94 93 95 open Globalenvs 96 97 open BitVectorTrie 94 98 95 99 open CostLabel … … 776 780 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 777 781  Kstop > h_Kstop 778  Kseq (x_ 5937, x_5936) >779 h_Kseq x_ 5937 x_5936782  Kseq (x_8622, x_8621) > 783 h_Kseq x_8622 x_8621 780 784 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 781 h_Kswitch h_Kcall x_ 5936)782  Kwhile (x_ 5940, x_5939, x_5938) >783 h_Kwhile x_ 5940 x_5939 x_5938785 h_Kswitch h_Kcall x_8621) 786  Kwhile (x_8625, x_8624, x_8623) > 787 h_Kwhile x_8625 x_8624 x_8623 784 788 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 785 h_Kswitch h_Kcall x_ 5938)786  Kdowhile (x_ 5943, x_5942, x_5941) >787 h_Kdowhile x_ 5943 x_5942 x_5941789 h_Kswitch h_Kcall x_8623) 790  Kdowhile (x_8628, x_8627, x_8626) > 791 h_Kdowhile x_8628 x_8627 x_8626 788 792 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 789 h_Kswitch h_Kcall x_ 5941)790  Kfor2 (x_ 5947, x_5946, x_5945, x_5944) >791 h_Kfor2 x_ 5947 x_5946 x_5945 x_5944793 h_Kswitch h_Kcall x_8626) 794  Kfor2 (x_8632, x_8631, x_8630, x_8629) > 795 h_Kfor2 x_8632 x_8631 x_8630 x_8629 792 796 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 793 h_Kswitch h_Kcall x_ 5944)794  Kfor3 (x_ 5951, x_5950, x_5949, x_5948) >795 h_Kfor3 x_ 5951 x_5950 x_5949 x_5948797 h_Kswitch h_Kcall x_8629) 798  Kfor3 (x_8636, x_8635, x_8634, x_8633) > 799 h_Kfor3 x_8636 x_8635 x_8634 x_8633 796 800 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 797 h_Kswitch h_Kcall x_ 5948)798  Kswitch x_ 5952>799 h_Kswitch x_ 5952801 h_Kswitch h_Kcall x_8633) 802  Kswitch x_8637 > 803 h_Kswitch x_8637 800 804 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 801 h_Kswitch h_Kcall x_ 5952)802  Kcall (x_ 5956, x_5955, x_5954, x_5953) >803 h_Kcall x_ 5956 x_5955 x_5954 x_5953805 h_Kswitch h_Kcall x_8637) 806  Kcall (x_8641, x_8640, x_8639, x_8638) > 807 h_Kcall x_8641 x_8640 x_8639 x_8638 804 808 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 805 h_Kswitch h_Kcall x_ 5953)809 h_Kswitch h_Kcall x_8638) 806 810 807 811 (** val cont_rect_Type3 : … … 816 820 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 817 821  Kstop > h_Kstop 818  Kseq (x_ 5997, x_5996) >819 h_Kseq x_ 5997 x_5996822  Kseq (x_8682, x_8681) > 823 h_Kseq x_8682 x_8681 820 824 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 821 h_Kswitch h_Kcall x_ 5996)822  Kwhile (x_ 6000, x_5999, x_5998) >823 h_Kwhile x_ 6000 x_5999 x_5998825 h_Kswitch h_Kcall x_8681) 826  Kwhile (x_8685, x_8684, x_8683) > 827 h_Kwhile x_8685 x_8684 x_8683 824 828 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 825 h_Kswitch h_Kcall x_ 5998)826  Kdowhile (x_ 6003, x_6002, x_6001) >827 h_Kdowhile x_ 6003 x_6002 x_6001829 h_Kswitch h_Kcall x_8683) 830  Kdowhile (x_8688, x_8687, x_8686) > 831 h_Kdowhile x_8688 x_8687 x_8686 828 832 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 829 h_Kswitch h_Kcall x_ 6001)830  Kfor2 (x_ 6007, x_6006, x_6005, x_6004) >831 h_Kfor2 x_ 6007 x_6006 x_6005 x_6004833 h_Kswitch h_Kcall x_8686) 834  Kfor2 (x_8692, x_8691, x_8690, x_8689) > 835 h_Kfor2 x_8692 x_8691 x_8690 x_8689 832 836 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 833 h_Kswitch h_Kcall x_ 6004)834  Kfor3 (x_ 6011, x_6010, x_6009, x_6008) >835 h_Kfor3 x_ 6011 x_6010 x_6009 x_6008837 h_Kswitch h_Kcall x_8689) 838  Kfor3 (x_8696, x_8695, x_8694, x_8693) > 839 h_Kfor3 x_8696 x_8695 x_8694 x_8693 836 840 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 837 h_Kswitch h_Kcall x_ 6008)838  Kswitch x_ 6012>839 h_Kswitch x_ 6012841 h_Kswitch h_Kcall x_8693) 842  Kswitch x_8697 > 843 h_Kswitch x_8697 840 844 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 841 h_Kswitch h_Kcall x_ 6012)842  Kcall (x_ 6016, x_6015, x_6014, x_6013) >843 h_Kcall x_ 6016 x_6015 x_6014 x_6013845 h_Kswitch h_Kcall x_8697) 846  Kcall (x_8701, x_8700, x_8699, x_8698) > 847 h_Kcall x_8701 x_8700 x_8699 x_8698 844 848 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 845 h_Kswitch h_Kcall x_ 6013)849 h_Kswitch h_Kcall x_8698) 846 850 847 851 (** val cont_rect_Type2 : … … 856 860 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 857 861  Kstop > h_Kstop 858  Kseq (x_ 6027, x_6026) >859 h_Kseq x_ 6027 x_6026862  Kseq (x_8712, x_8711) > 863 h_Kseq x_8712 x_8711 860 864 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 861 h_Kswitch h_Kcall x_ 6026)862  Kwhile (x_ 6030, x_6029, x_6028) >863 h_Kwhile x_ 6030 x_6029 x_6028865 h_Kswitch h_Kcall x_8711) 866  Kwhile (x_8715, x_8714, x_8713) > 867 h_Kwhile x_8715 x_8714 x_8713 864 868 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 865 h_Kswitch h_Kcall x_ 6028)866  Kdowhile (x_ 6033, x_6032, x_6031) >867 h_Kdowhile x_ 6033 x_6032 x_6031869 h_Kswitch h_Kcall x_8713) 870  Kdowhile (x_8718, x_8717, x_8716) > 871 h_Kdowhile x_8718 x_8717 x_8716 868 872 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 869 h_Kswitch h_Kcall x_ 6031)870  Kfor2 (x_ 6037, x_6036, x_6035, x_6034) >871 h_Kfor2 x_ 6037 x_6036 x_6035 x_6034873 h_Kswitch h_Kcall x_8716) 874  Kfor2 (x_8722, x_8721, x_8720, x_8719) > 875 h_Kfor2 x_8722 x_8721 x_8720 x_8719 872 876 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 873 h_Kswitch h_Kcall x_ 6034)874  Kfor3 (x_ 6041, x_6040, x_6039, x_6038) >875 h_Kfor3 x_ 6041 x_6040 x_6039 x_6038877 h_Kswitch h_Kcall x_8719) 878  Kfor3 (x_8726, x_8725, x_8724, x_8723) > 879 h_Kfor3 x_8726 x_8725 x_8724 x_8723 876 880 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 877 h_Kswitch h_Kcall x_ 6038)878  Kswitch x_ 6042>879 h_Kswitch x_ 6042881 h_Kswitch h_Kcall x_8723) 882  Kswitch x_8727 > 883 h_Kswitch x_8727 880 884 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 881 h_Kswitch h_Kcall x_ 6042)882  Kcall (x_ 6046, x_6045, x_6044, x_6043) >883 h_Kcall x_ 6046 x_6045 x_6044 x_6043885 h_Kswitch h_Kcall x_8727) 886  Kcall (x_8731, x_8730, x_8729, x_8728) > 887 h_Kcall x_8731 x_8730 x_8729 x_8728 884 888 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 885 h_Kswitch h_Kcall x_ 6043)889 h_Kswitch h_Kcall x_8728) 886 890 887 891 (** val cont_rect_Type1 : … … 896 900 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 897 901  Kstop > h_Kstop 898  Kseq (x_ 6057, x_6056) >899 h_Kseq x_ 6057 x_6056902  Kseq (x_8742, x_8741) > 903 h_Kseq x_8742 x_8741 900 904 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 901 h_Kswitch h_Kcall x_ 6056)902  Kwhile (x_ 6060, x_6059, x_6058) >903 h_Kwhile x_ 6060 x_6059 x_6058905 h_Kswitch h_Kcall x_8741) 906  Kwhile (x_8745, x_8744, x_8743) > 907 h_Kwhile x_8745 x_8744 x_8743 904 908 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 905 h_Kswitch h_Kcall x_ 6058)906  Kdowhile (x_ 6063, x_6062, x_6061) >907 h_Kdowhile x_ 6063 x_6062 x_6061909 h_Kswitch h_Kcall x_8743) 910  Kdowhile (x_8748, x_8747, x_8746) > 911 h_Kdowhile x_8748 x_8747 x_8746 908 912 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 909 h_Kswitch h_Kcall x_ 6061)910  Kfor2 (x_ 6067, x_6066, x_6065, x_6064) >911 h_Kfor2 x_ 6067 x_6066 x_6065 x_6064913 h_Kswitch h_Kcall x_8746) 914  Kfor2 (x_8752, x_8751, x_8750, x_8749) > 915 h_Kfor2 x_8752 x_8751 x_8750 x_8749 912 916 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 913 h_Kswitch h_Kcall x_ 6064)914  Kfor3 (x_ 6071, x_6070, x_6069, x_6068) >915 h_Kfor3 x_ 6071 x_6070 x_6069 x_6068917 h_Kswitch h_Kcall x_8749) 918  Kfor3 (x_8756, x_8755, x_8754, x_8753) > 919 h_Kfor3 x_8756 x_8755 x_8754 x_8753 916 920 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 917 h_Kswitch h_Kcall x_ 6068)918  Kswitch x_ 6072>919 h_Kswitch x_ 6072921 h_Kswitch h_Kcall x_8753) 922  Kswitch x_8757 > 923 h_Kswitch x_8757 920 924 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 921 h_Kswitch h_Kcall x_ 6072)922  Kcall (x_ 6076, x_6075, x_6074, x_6073) >923 h_Kcall x_ 6076 x_6075 x_6074 x_6073925 h_Kswitch h_Kcall x_8757) 926  Kcall (x_8761, x_8760, x_8759, x_8758) > 927 h_Kcall x_8761 x_8760 x_8759 x_8758 924 928 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 925 h_Kswitch h_Kcall x_ 6073)929 h_Kswitch h_Kcall x_8758) 926 930 927 931 (** val cont_rect_Type0 : … … 936 940 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 937 941  Kstop > h_Kstop 938  Kseq (x_ 6087, x_6086) >939 h_Kseq x_ 6087 x_6086942  Kseq (x_8772, x_8771) > 943 h_Kseq x_8772 x_8771 940 944 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 941 h_Kswitch h_Kcall x_ 6086)942  Kwhile (x_ 6090, x_6089, x_6088) >943 h_Kwhile x_ 6090 x_6089 x_6088945 h_Kswitch h_Kcall x_8771) 946  Kwhile (x_8775, x_8774, x_8773) > 947 h_Kwhile x_8775 x_8774 x_8773 944 948 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 945 h_Kswitch h_Kcall x_ 6088)946  Kdowhile (x_ 6093, x_6092, x_6091) >947 h_Kdowhile x_ 6093 x_6092 x_6091949 h_Kswitch h_Kcall x_8773) 950  Kdowhile (x_8778, x_8777, x_8776) > 951 h_Kdowhile x_8778 x_8777 x_8776 948 952 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 949 h_Kswitch h_Kcall x_ 6091)950  Kfor2 (x_ 6097, x_6096, x_6095, x_6094) >951 h_Kfor2 x_ 6097 x_6096 x_6095 x_6094953 h_Kswitch h_Kcall x_8776) 954  Kfor2 (x_8782, x_8781, x_8780, x_8779) > 955 h_Kfor2 x_8782 x_8781 x_8780 x_8779 952 956 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 953 h_Kswitch h_Kcall x_ 6094)954  Kfor3 (x_ 6101, x_6100, x_6099, x_6098) >955 h_Kfor3 x_ 6101 x_6100 x_6099 x_6098957 h_Kswitch h_Kcall x_8779) 958  Kfor3 (x_8786, x_8785, x_8784, x_8783) > 959 h_Kfor3 x_8786 x_8785 x_8784 x_8783 956 960 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 957 h_Kswitch h_Kcall x_ 6098)958  Kswitch x_ 6102>959 h_Kswitch x_ 6102961 h_Kswitch h_Kcall x_8783) 962  Kswitch x_8787 > 963 h_Kswitch x_8787 960 964 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 961 h_Kswitch h_Kcall x_ 6102)962  Kcall (x_ 6106, x_6105, x_6104, x_6103) >963 h_Kcall x_ 6106 x_6105 x_6104 x_6103965 h_Kswitch h_Kcall x_8787) 966  Kcall (x_8791, x_8790, x_8789, x_8788) > 967 h_Kcall x_8791 x_8790 x_8789 x_8788 964 968 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 965 h_Kswitch h_Kcall x_ 6103)969 h_Kswitch h_Kcall x_8788) 966 970 967 971 (** val cont_inv_rect_Type4 : … … 1069 1073 type state0 = 1070 1074  State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1 1071  Callstate of Csyntax.clight_fundef * Values.val0 List.list * cont1072 * GenMem.mem11075  Callstate of Values.val0 * Csyntax.clight_fundef * Values.val0 List.list 1076 * cont * GenMem.mem1 1073 1077  Returnstate of Values.val0 * cont * GenMem.mem1 1074 1078  Finalstate of Integers.int … … 1076 1080 (** val state_rect_Type4 : 1077 1081 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1078 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1079 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1080 (Integers.int > 'a1) > state0 > 'a1 **)1082 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1083 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1084 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1081 1085 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function 1082 1086  State (f, s, k, e1, m) > h_State f s k e1 m 1083  Callstate (f d, args, k, m) > h_Callstatefd args k m1087  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1084 1088  Returnstate (res1, k, m) > h_Returnstate res1 k m 1085 1089  Finalstate r > h_Finalstate r … … 1087 1091 (** val state_rect_Type5 : 1088 1092 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1089 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1090 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1091 (Integers.int > 'a1) > state0 > 'a1 **)1093 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1094 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1095 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1092 1096 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function 1093 1097  State (f, s, k, e1, m) > h_State f s k e1 m 1094  Callstate (f d, args, k, m) > h_Callstatefd args k m1098  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1095 1099  Returnstate (res1, k, m) > h_Returnstate res1 k m 1096 1100  Finalstate r > h_Finalstate r … … 1098 1102 (** val state_rect_Type3 : 1099 1103 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1100 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1101 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1102 (Integers.int > 'a1) > state0 > 'a1 **)1104 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1105 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1106 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1103 1107 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function 1104 1108  State (f, s, k, e1, m) > h_State f s k e1 m 1105  Callstate (f d, args, k, m) > h_Callstatefd args k m1109  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1106 1110  Returnstate (res1, k, m) > h_Returnstate res1 k m 1107 1111  Finalstate r > h_Finalstate r … … 1109 1113 (** val state_rect_Type2 : 1110 1114 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1111 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1112 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1113 (Integers.int > 'a1) > state0 > 'a1 **)1115 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1116 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1117 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1114 1118 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function 1115 1119  State (f, s, k, e1, m) > h_State f s k e1 m 1116  Callstate (f d, args, k, m) > h_Callstatefd args k m1120  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1117 1121  Returnstate (res1, k, m) > h_Returnstate res1 k m 1118 1122  Finalstate r > h_Finalstate r … … 1120 1124 (** val state_rect_Type1 : 1121 1125 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1122 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1123 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1124 (Integers.int > 'a1) > state0 > 'a1 **)1126 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1127 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1128 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1125 1129 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function 1126 1130  State (f, s, k, e1, m) > h_State f s k e1 m 1127  Callstate (f d, args, k, m) > h_Callstatefd args k m1131  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1128 1132  Returnstate (res1, k, m) > h_Returnstate res1 k m 1129 1133  Finalstate r > h_Finalstate r … … 1131 1135 (** val state_rect_Type0 : 1132 1136 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1133 'a1) > ( Csyntax.clight_fundef > Values.val0 List.list > cont >1134 GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 'a1)>1135 (Integers.int > 'a1) > state0 > 'a1 **)1137 'a1) > (Values.val0 > Csyntax.clight_fundef > Values.val0 List.list > 1138 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1139 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1136 1140 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function 1137 1141  State (f, s, k, e1, m) > h_State f s k e1 m 1138  Callstate (f d, args, k, m) > h_Callstatefd args k m1142  Callstate (fb, fd, args, k, m) > h_Callstate fb fd args k m 1139 1143  Returnstate (res1, k, m) > h_Returnstate res1 k m 1140 1144  Finalstate r > h_Finalstate r … … 1142 1146 (** val state_inv_rect_Type4 : 1143 1147 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1144 GenMem.mem1 > __ > 'a1) > (Csyntax.clight_fundef > Values.val0 1145 List.list > cont > GenMem.mem1 > __ > 'a1) > (Values.val0 > cont > 1146 GenMem.mem1 > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 **) 1148 GenMem.mem1 > __ > 'a1) > (Values.val0 > Csyntax.clight_fundef > 1149 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1150 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ 1151 > 'a1) > 'a1 **) 1147 1152 let state_inv_rect_Type4 hterm h1 h2 h3 h4 = 1148 1153 let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __ … … 1150 1155 (** val state_inv_rect_Type3 : 1151 1156 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1152 GenMem.mem1 > __ > 'a1) > (Csyntax.clight_fundef > Values.val0 1153 List.list > cont > GenMem.mem1 > __ > 'a1) > (Values.val0 > cont > 1154 GenMem.mem1 > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 **) 1157 GenMem.mem1 > __ > 'a1) > (Values.val0 > Csyntax.clight_fundef > 1158 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1159 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ 1160 > 'a1) > 'a1 **) 1155 1161 let state_inv_rect_Type3 hterm h1 h2 h3 h4 = 1156 1162 let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __ … … 1158 1164 (** val state_inv_rect_Type2 : 1159 1165 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1160 GenMem.mem1 > __ > 'a1) > (Csyntax.clight_fundef > Values.val0 1161 List.list > cont > GenMem.mem1 > __ > 'a1) > (Values.val0 > cont > 1162 GenMem.mem1 > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 **) 1166 GenMem.mem1 > __ > 'a1) > (Values.val0 > Csyntax.clight_fundef > 1167 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1168 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ 1169 > 'a1) > 'a1 **) 1163 1170 let state_inv_rect_Type2 hterm h1 h2 h3 h4 = 1164 1171 let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __ … … 1166 1173 (** val state_inv_rect_Type1 : 1167 1174 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1168 GenMem.mem1 > __ > 'a1) > (Csyntax.clight_fundef > Values.val0 1169 List.list > cont > GenMem.mem1 > __ > 'a1) > (Values.val0 > cont > 1170 GenMem.mem1 > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 **) 1175 GenMem.mem1 > __ > 'a1) > (Values.val0 > Csyntax.clight_fundef > 1176 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1177 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ 1178 > 'a1) > 'a1 **) 1171 1179 let state_inv_rect_Type1 hterm h1 h2 h3 h4 = 1172 1180 let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __ … … 1174 1182 (** val state_inv_rect_Type0 : 1175 1183 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1176 GenMem.mem1 > __ > 'a1) > (Csyntax.clight_fundef > Values.val0 1177 List.list > cont > GenMem.mem1 > __ > 'a1) > (Values.val0 > cont > 1178 GenMem.mem1 > __ > 'a1) > (Integers.int > __ > 'a1) > 'a1 **) 1184 GenMem.mem1 > __ > 'a1) > (Values.val0 > Csyntax.clight_fundef > 1185 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1186 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ 1187 > 'a1) > 'a1 **) 1179 1188 let state_inv_rect_Type0 hterm h1 h2 h3 h4 = 1180 1189 let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __ … … 1186 1195  State (a0, a1, a2, a3, a4) > 1187 1196 Obj.magic (fun _ dH > dH __ __ __ __ __) 1188  Callstate (a0, a1, a2, a3) > Obj.magic (fun _ dH > dH __ __ __ __) 1197  Callstate (a0, a1, a2, a3, a4) > 1198 Obj.magic (fun _ dH > dH __ __ __ __ __) 1189 1199  Returnstate (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 1190 1200  Finalstate a0 > Obj.magic (fun _ dH > dH __)) y … … 1196 1206  State (a0, a1, a2, a3, a4) > 1197 1207 Obj.magic (fun _ dH > dH __ __ __ __ __) 1198  Callstate (a0, a1, a2, a3) > Obj.magic (fun _ dH > dH __ __ __ __) 1208  Callstate (a0, a1, a2, a3, a4) > 1209 Obj.magic (fun _ dH > dH __ __ __ __ __) 1199 1210  Returnstate (a0, a1, a2) > Obj.magic (fun _ dH > dH __ __ __) 1200 1211  Finalstate a0 > Obj.magic (fun _ dH > dH __)) y
Note: See TracChangeset
for help on using the changeset viewer.