Changeset 2730 for extracted/csem.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/csem.ml
r2717 r2730 780 780 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 781 781  Kstop > h_Kstop 782  Kseq (x_ 8622, x_8621) >783 h_Kseq x_ 8622 x_8621782  Kseq (x_6713, x_6712) > 783 h_Kseq x_6713 x_6712 784 784 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 785 h_Kswitch h_Kcall x_ 8621)786  Kwhile (x_ 8625, x_8624, x_8623) >787 h_Kwhile x_ 8625 x_8624 x_8623785 h_Kswitch h_Kcall x_6712) 786  Kwhile (x_6716, x_6715, x_6714) > 787 h_Kwhile x_6716 x_6715 x_6714 788 788 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 789 h_Kswitch h_Kcall x_ 8623)790  Kdowhile (x_ 8628, x_8627, x_8626) >791 h_Kdowhile x_ 8628 x_8627 x_8626789 h_Kswitch h_Kcall x_6714) 790  Kdowhile (x_6719, x_6718, x_6717) > 791 h_Kdowhile x_6719 x_6718 x_6717 792 792 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 793 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_8629793 h_Kswitch h_Kcall x_6717) 794  Kfor2 (x_6723, x_6722, x_6721, x_6720) > 795 h_Kfor2 x_6723 x_6722 x_6721 x_6720 796 796 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 797 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_8633797 h_Kswitch h_Kcall x_6720) 798  Kfor3 (x_6727, x_6726, x_6725, x_6724) > 799 h_Kfor3 x_6727 x_6726 x_6725 x_6724 800 800 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 801 h_Kswitch h_Kcall x_ 8633)802  Kswitch x_ 8637>803 h_Kswitch x_ 8637801 h_Kswitch h_Kcall x_6724) 802  Kswitch x_6728 > 803 h_Kswitch x_6728 804 804 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 805 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_8638805 h_Kswitch h_Kcall x_6728) 806  Kcall (x_6732, x_6731, x_6730, x_6729) > 807 h_Kcall x_6732 x_6731 x_6730 x_6729 808 808 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 809 h_Kswitch h_Kcall x_ 8638)809 h_Kswitch h_Kcall x_6729) 810 810 811 811 (** val cont_rect_Type3 : … … 820 820 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 821 821  Kstop > h_Kstop 822  Kseq (x_ 8682, x_8681) >823 h_Kseq x_ 8682 x_8681822  Kseq (x_6773, x_6772) > 823 h_Kseq x_6773 x_6772 824 824 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 825 h_Kswitch h_Kcall x_ 8681)826  Kwhile (x_ 8685, x_8684, x_8683) >827 h_Kwhile x_ 8685 x_8684 x_8683825 h_Kswitch h_Kcall x_6772) 826  Kwhile (x_6776, x_6775, x_6774) > 827 h_Kwhile x_6776 x_6775 x_6774 828 828 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 829 h_Kswitch h_Kcall x_ 8683)830  Kdowhile (x_ 8688, x_8687, x_8686) >831 h_Kdowhile x_ 8688 x_8687 x_8686829 h_Kswitch h_Kcall x_6774) 830  Kdowhile (x_6779, x_6778, x_6777) > 831 h_Kdowhile x_6779 x_6778 x_6777 832 832 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 833 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_8689833 h_Kswitch h_Kcall x_6777) 834  Kfor2 (x_6783, x_6782, x_6781, x_6780) > 835 h_Kfor2 x_6783 x_6782 x_6781 x_6780 836 836 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 837 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_8693837 h_Kswitch h_Kcall x_6780) 838  Kfor3 (x_6787, x_6786, x_6785, x_6784) > 839 h_Kfor3 x_6787 x_6786 x_6785 x_6784 840 840 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 841 h_Kswitch h_Kcall x_ 8693)842  Kswitch x_ 8697>843 h_Kswitch x_ 8697841 h_Kswitch h_Kcall x_6784) 842  Kswitch x_6788 > 843 h_Kswitch x_6788 844 844 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 845 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_8698845 h_Kswitch h_Kcall x_6788) 846  Kcall (x_6792, x_6791, x_6790, x_6789) > 847 h_Kcall x_6792 x_6791 x_6790 x_6789 848 848 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 849 h_Kswitch h_Kcall x_ 8698)849 h_Kswitch h_Kcall x_6789) 850 850 851 851 (** val cont_rect_Type2 : … … 860 860 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 861 861  Kstop > h_Kstop 862  Kseq (x_ 8712, x_8711) >863 h_Kseq x_ 8712 x_8711862  Kseq (x_6803, x_6802) > 863 h_Kseq x_6803 x_6802 864 864 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 865 h_Kswitch h_Kcall x_ 8711)866  Kwhile (x_ 8715, x_8714, x_8713) >867 h_Kwhile x_ 8715 x_8714 x_8713865 h_Kswitch h_Kcall x_6802) 866  Kwhile (x_6806, x_6805, x_6804) > 867 h_Kwhile x_6806 x_6805 x_6804 868 868 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 869 h_Kswitch h_Kcall x_ 8713)870  Kdowhile (x_ 8718, x_8717, x_8716) >871 h_Kdowhile x_ 8718 x_8717 x_8716869 h_Kswitch h_Kcall x_6804) 870  Kdowhile (x_6809, x_6808, x_6807) > 871 h_Kdowhile x_6809 x_6808 x_6807 872 872 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 873 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_8719873 h_Kswitch h_Kcall x_6807) 874  Kfor2 (x_6813, x_6812, x_6811, x_6810) > 875 h_Kfor2 x_6813 x_6812 x_6811 x_6810 876 876 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 877 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_8723877 h_Kswitch h_Kcall x_6810) 878  Kfor3 (x_6817, x_6816, x_6815, x_6814) > 879 h_Kfor3 x_6817 x_6816 x_6815 x_6814 880 880 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 881 h_Kswitch h_Kcall x_ 8723)882  Kswitch x_ 8727>883 h_Kswitch x_ 8727881 h_Kswitch h_Kcall x_6814) 882  Kswitch x_6818 > 883 h_Kswitch x_6818 884 884 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 885 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_8728885 h_Kswitch h_Kcall x_6818) 886  Kcall (x_6822, x_6821, x_6820, x_6819) > 887 h_Kcall x_6822 x_6821 x_6820 x_6819 888 888 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 889 h_Kswitch h_Kcall x_ 8728)889 h_Kswitch h_Kcall x_6819) 890 890 891 891 (** val cont_rect_Type1 : … … 900 900 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 901 901  Kstop > h_Kstop 902  Kseq (x_ 8742, x_8741) >903 h_Kseq x_ 8742 x_8741902  Kseq (x_6833, x_6832) > 903 h_Kseq x_6833 x_6832 904 904 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 905 h_Kswitch h_Kcall x_ 8741)906  Kwhile (x_ 8745, x_8744, x_8743) >907 h_Kwhile x_ 8745 x_8744 x_8743905 h_Kswitch h_Kcall x_6832) 906  Kwhile (x_6836, x_6835, x_6834) > 907 h_Kwhile x_6836 x_6835 x_6834 908 908 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 909 h_Kswitch h_Kcall x_ 8743)910  Kdowhile (x_ 8748, x_8747, x_8746) >911 h_Kdowhile x_ 8748 x_8747 x_8746909 h_Kswitch h_Kcall x_6834) 910  Kdowhile (x_6839, x_6838, x_6837) > 911 h_Kdowhile x_6839 x_6838 x_6837 912 912 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 913 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_8749913 h_Kswitch h_Kcall x_6837) 914  Kfor2 (x_6843, x_6842, x_6841, x_6840) > 915 h_Kfor2 x_6843 x_6842 x_6841 x_6840 916 916 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 917 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_8753917 h_Kswitch h_Kcall x_6840) 918  Kfor3 (x_6847, x_6846, x_6845, x_6844) > 919 h_Kfor3 x_6847 x_6846 x_6845 x_6844 920 920 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 921 h_Kswitch h_Kcall x_ 8753)922  Kswitch x_ 8757>923 h_Kswitch x_ 8757921 h_Kswitch h_Kcall x_6844) 922  Kswitch x_6848 > 923 h_Kswitch x_6848 924 924 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 925 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_8758925 h_Kswitch h_Kcall x_6848) 926  Kcall (x_6852, x_6851, x_6850, x_6849) > 927 h_Kcall x_6852 x_6851 x_6850 x_6849 928 928 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 929 h_Kswitch h_Kcall x_ 8758)929 h_Kswitch h_Kcall x_6849) 930 930 931 931 (** val cont_rect_Type0 : … … 940 940 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 941 941  Kstop > h_Kstop 942  Kseq (x_ 8772, x_8771) >943 h_Kseq x_ 8772 x_8771942  Kseq (x_6863, x_6862) > 943 h_Kseq x_6863 x_6862 944 944 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 945 h_Kswitch h_Kcall x_ 8771)946  Kwhile (x_ 8775, x_8774, x_8773) >947 h_Kwhile x_ 8775 x_8774 x_8773945 h_Kswitch h_Kcall x_6862) 946  Kwhile (x_6866, x_6865, x_6864) > 947 h_Kwhile x_6866 x_6865 x_6864 948 948 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 949 h_Kswitch h_Kcall x_ 8773)950  Kdowhile (x_ 8778, x_8777, x_8776) >951 h_Kdowhile x_ 8778 x_8777 x_8776949 h_Kswitch h_Kcall x_6864) 950  Kdowhile (x_6869, x_6868, x_6867) > 951 h_Kdowhile x_6869 x_6868 x_6867 952 952 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 953 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_8779953 h_Kswitch h_Kcall x_6867) 954  Kfor2 (x_6873, x_6872, x_6871, x_6870) > 955 h_Kfor2 x_6873 x_6872 x_6871 x_6870 956 956 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 957 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_8783957 h_Kswitch h_Kcall x_6870) 958  Kfor3 (x_6877, x_6876, x_6875, x_6874) > 959 h_Kfor3 x_6877 x_6876 x_6875 x_6874 960 960 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 961 h_Kswitch h_Kcall x_ 8783)962  Kswitch x_ 8787>963 h_Kswitch x_ 8787961 h_Kswitch h_Kcall x_6874) 962  Kswitch x_6878 > 963 h_Kswitch x_6878 964 964 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 965 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_8788965 h_Kswitch h_Kcall x_6878) 966  Kcall (x_6882, x_6881, x_6880, x_6879) > 967 h_Kcall x_6882 x_6881 x_6880 x_6879 968 968 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 969 h_Kswitch h_Kcall x_ 8788)969 h_Kswitch h_Kcall x_6879) 970 970 971 971 (** val cont_inv_rect_Type4 : … … 1073 1073 type state0 = 1074 1074  State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1 1075  Callstate of Values.val0* Csyntax.clight_fundef * Values.val0 List.list1075  Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list 1076 1076 * cont * GenMem.mem1 1077 1077  Returnstate of Values.val0 * cont * GenMem.mem1 … … 1080 1080 (** val state_rect_Type4 : 1081 1081 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1082 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1082 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1083 1083 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1084 1084 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1085 1085 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function 1086 1086  State (f, s, k, e1, m) > h_State f s k e1 m 1087  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1087  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1088 1088  Returnstate (res1, k, m) > h_Returnstate res1 k m 1089 1089  Finalstate r > h_Finalstate r … … 1091 1091 (** val state_rect_Type5 : 1092 1092 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1093 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1093 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1094 1094 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1095 1095 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1096 1096 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function 1097 1097  State (f, s, k, e1, m) > h_State f s k e1 m 1098  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1098  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1099 1099  Returnstate (res1, k, m) > h_Returnstate res1 k m 1100 1100  Finalstate r > h_Finalstate r … … 1102 1102 (** val state_rect_Type3 : 1103 1103 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1104 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1104 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1105 1105 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1106 1106 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1107 1107 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function 1108 1108  State (f, s, k, e1, m) > h_State f s k e1 m 1109  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1109  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1110 1110  Returnstate (res1, k, m) > h_Returnstate res1 k m 1111 1111  Finalstate r > h_Finalstate r … … 1113 1113 (** val state_rect_Type2 : 1114 1114 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1115 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1115 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1116 1116 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1117 1117 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1118 1118 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function 1119 1119  State (f, s, k, e1, m) > h_State f s k e1 m 1120  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1120  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1121 1121  Returnstate (res1, k, m) > h_Returnstate res1 k m 1122 1122  Finalstate r > h_Finalstate r … … 1124 1124 (** val state_rect_Type1 : 1125 1125 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1126 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1126 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1127 1127 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1128 1128 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1129 1129 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function 1130 1130  State (f, s, k, e1, m) > h_State f s k e1 m 1131  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1131  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1132 1132  Returnstate (res1, k, m) > h_Returnstate res1 k m 1133 1133  Finalstate r > h_Finalstate r … … 1135 1135 (** val state_rect_Type0 : 1136 1136 (Csyntax.function0 > Csyntax.statement > cont > env > GenMem.mem1 > 1137 'a1) > ( Values.val0> Csyntax.clight_fundef > Values.val0 List.list >1137 'a1) > (AST.ident > Csyntax.clight_fundef > Values.val0 List.list > 1138 1138 cont > GenMem.mem1 > 'a1) > (Values.val0 > cont > GenMem.mem1 > 1139 1139 'a1) > (Integers.int > 'a1) > state0 > 'a1 **) 1140 1140 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function 1141 1141  State (f, s, k, e1, m) > h_State f s k e1 m 1142  Callstate ( fb, fd, args, k, m) > h_Callstate fbfd args k m1142  Callstate (id, fd, args, k, m) > h_Callstate id fd args k m 1143 1143  Returnstate (res1, k, m) > h_Returnstate res1 k m 1144 1144  Finalstate r > h_Finalstate r … … 1146 1146 (** val state_inv_rect_Type4 : 1147 1147 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1148 GenMem.mem1 > __ > 'a1) > ( Values.val0> Csyntax.clight_fundef >1148 GenMem.mem1 > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 1149 1149 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1150 1150 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ … … 1155 1155 (** val state_inv_rect_Type3 : 1156 1156 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1157 GenMem.mem1 > __ > 'a1) > ( Values.val0> Csyntax.clight_fundef >1157 GenMem.mem1 > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 1158 1158 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1159 1159 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ … … 1164 1164 (** val state_inv_rect_Type2 : 1165 1165 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1166 GenMem.mem1 > __ > 'a1) > ( Values.val0> Csyntax.clight_fundef >1166 GenMem.mem1 > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 1167 1167 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1168 1168 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ … … 1173 1173 (** val state_inv_rect_Type1 : 1174 1174 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1175 GenMem.mem1 > __ > 'a1) > ( Values.val0> Csyntax.clight_fundef >1175 GenMem.mem1 > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 1176 1176 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1177 1177 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __ … … 1182 1182 (** val state_inv_rect_Type0 : 1183 1183 state0 > (Csyntax.function0 > Csyntax.statement > cont > env > 1184 GenMem.mem1 > __ > 'a1) > ( Values.val0> Csyntax.clight_fundef >1184 GenMem.mem1 > __ > 'a1) > (AST.ident > Csyntax.clight_fundef > 1185 1185 Values.val0 List.list > cont > GenMem.mem1 > __ > 'a1) > 1186 1186 (Values.val0 > cont > GenMem.mem1 > __ > 'a1) > (Integers.int > __
Note: See TracChangeset
for help on using the changeset viewer.