Changeset 2649 for extracted/csem.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/csem.ml
r2601 r2649 3 3 open Extra_bool 4 4 5 open Coqlib 6 5 7 open Values 6 8 … … 35 37 open Identifiers 36 38 37 open Coqlib38 39 open Floats40 41 39 open Arithmetic 42 40 … … 57 55 open AST 58 56 57 open ErrorMessages 58 59 59 open Option 60 60 … … 68 68 69 69 open Positive 70 71 open Char72 73 open String74 70 75 71 open PreIdentifiers … … 710 706 (** val empty_env : env **) 711 707 let empty_env = 712 Identifiers.empty_map AST.symbolTag708 Identifiers.empty_map PreIdentifiers.SymbolTag 713 709 714 710 (** val load_value_of_type : … … 737 733 (** val blocks_of_env : env > Pointers.block List.list **) 738 734 let blocks_of_env e1 = 739 List.map (fun x > x.Types.snd) (Identifiers.elements AST.symbolTag e1) 735 List.map (fun x > x.Types.snd) 736 (Identifiers.elements PreIdentifiers.SymbolTag e1) 740 737 741 738 (** val select_switch : … … 779 776 let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 780 777  Kstop > h_Kstop 781  Kseq (x_ 7621, x_7620) >782 h_Kseq x_ 7621 x_7620778  Kseq (x_5937, x_5936) > 779 h_Kseq x_5937 x_5936 783 780 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 784 h_Kswitch h_Kcall x_ 7620)785  Kwhile (x_ 7624, x_7623, x_7622) >786 h_Kwhile x_ 7624 x_7623 x_7622781 h_Kswitch h_Kcall x_5936) 782  Kwhile (x_5940, x_5939, x_5938) > 783 h_Kwhile x_5940 x_5939 x_5938 787 784 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 788 h_Kswitch h_Kcall x_ 7622)789  Kdowhile (x_ 7627, x_7626, x_7625) >790 h_Kdowhile x_ 7627 x_7626 x_7625785 h_Kswitch h_Kcall x_5938) 786  Kdowhile (x_5943, x_5942, x_5941) > 787 h_Kdowhile x_5943 x_5942 x_5941 791 788 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 792 h_Kswitch h_Kcall x_ 7625)793  Kfor2 (x_ 7631, x_7630, x_7629, x_7628) >794 h_Kfor2 x_ 7631 x_7630 x_7629 x_7628789 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_5944 795 792 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 796 h_Kswitch h_Kcall x_ 7628)797  Kfor3 (x_ 7635, x_7634, x_7633, x_7632) >798 h_Kfor3 x_ 7635 x_7634 x_7633 x_7632793 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_5948 799 796 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 800 h_Kswitch h_Kcall x_ 7632)801  Kswitch x_ 7636>802 h_Kswitch x_ 7636797 h_Kswitch h_Kcall x_5948) 798  Kswitch x_5952 > 799 h_Kswitch x_5952 803 800 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 804 h_Kswitch h_Kcall x_ 7636)805  Kcall (x_ 7640, x_7639, x_7638, x_7637) >806 h_Kcall x_ 7640 x_7639 x_7638 x_7637801 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_5953 807 804 (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 808 h_Kswitch h_Kcall x_ 7637)805 h_Kswitch h_Kcall x_5953) 809 806 810 807 (** val cont_rect_Type3 : … … 819 816 let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 820 817  Kstop > h_Kstop 821  Kseq (x_ 7681, x_7680) >822 h_Kseq x_ 7681 x_7680818  Kseq (x_5997, x_5996) > 819 h_Kseq x_5997 x_5996 823 820 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 824 h_Kswitch h_Kcall x_ 7680)825  Kwhile (x_ 7684, x_7683, x_7682) >826 h_Kwhile x_ 7684 x_7683 x_7682821 h_Kswitch h_Kcall x_5996) 822  Kwhile (x_6000, x_5999, x_5998) > 823 h_Kwhile x_6000 x_5999 x_5998 827 824 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 828 h_Kswitch h_Kcall x_ 7682)829  Kdowhile (x_ 7687, x_7686, x_7685) >830 h_Kdowhile x_ 7687 x_7686 x_7685825 h_Kswitch h_Kcall x_5998) 826  Kdowhile (x_6003, x_6002, x_6001) > 827 h_Kdowhile x_6003 x_6002 x_6001 831 828 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 832 h_Kswitch h_Kcall x_ 7685)833  Kfor2 (x_ 7691, x_7690, x_7689, x_7688) >834 h_Kfor2 x_ 7691 x_7690 x_7689 x_7688829 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_6004 835 832 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 836 h_Kswitch h_Kcall x_ 7688)837  Kfor3 (x_ 7695, x_7694, x_7693, x_7692) >838 h_Kfor3 x_ 7695 x_7694 x_7693 x_7692833 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_6008 839 836 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 840 h_Kswitch h_Kcall x_ 7692)841  Kswitch x_ 7696>842 h_Kswitch x_ 7696837 h_Kswitch h_Kcall x_6008) 838  Kswitch x_6012 > 839 h_Kswitch x_6012 843 840 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 844 h_Kswitch h_Kcall x_ 7696)845  Kcall (x_ 7700, x_7699, x_7698, x_7697) >846 h_Kcall x_ 7700 x_7699 x_7698 x_7697841 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_6013 847 844 (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 848 h_Kswitch h_Kcall x_ 7697)845 h_Kswitch h_Kcall x_6013) 849 846 850 847 (** val cont_rect_Type2 : … … 859 856 let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 860 857  Kstop > h_Kstop 861  Kseq (x_ 7711, x_7710) >862 h_Kseq x_ 7711 x_7710858  Kseq (x_6027, x_6026) > 859 h_Kseq x_6027 x_6026 863 860 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 864 h_Kswitch h_Kcall x_ 7710)865  Kwhile (x_ 7714, x_7713, x_7712) >866 h_Kwhile x_ 7714 x_7713 x_7712861 h_Kswitch h_Kcall x_6026) 862  Kwhile (x_6030, x_6029, x_6028) > 863 h_Kwhile x_6030 x_6029 x_6028 867 864 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 868 h_Kswitch h_Kcall x_ 7712)869  Kdowhile (x_ 7717, x_7716, x_7715) >870 h_Kdowhile x_ 7717 x_7716 x_7715865 h_Kswitch h_Kcall x_6028) 866  Kdowhile (x_6033, x_6032, x_6031) > 867 h_Kdowhile x_6033 x_6032 x_6031 871 868 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 872 h_Kswitch h_Kcall x_ 7715)873  Kfor2 (x_ 7721, x_7720, x_7719, x_7718) >874 h_Kfor2 x_ 7721 x_7720 x_7719 x_7718869 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_6034 875 872 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 876 h_Kswitch h_Kcall x_ 7718)877  Kfor3 (x_ 7725, x_7724, x_7723, x_7722) >878 h_Kfor3 x_ 7725 x_7724 x_7723 x_7722873 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_6038 879 876 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 880 h_Kswitch h_Kcall x_ 7722)881  Kswitch x_ 7726>882 h_Kswitch x_ 7726877 h_Kswitch h_Kcall x_6038) 878  Kswitch x_6042 > 879 h_Kswitch x_6042 883 880 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 884 h_Kswitch h_Kcall x_ 7726)885  Kcall (x_ 7730, x_7729, x_7728, x_7727) >886 h_Kcall x_ 7730 x_7729 x_7728 x_7727881 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_6043 887 884 (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 888 h_Kswitch h_Kcall x_ 7727)885 h_Kswitch h_Kcall x_6043) 889 886 890 887 (** val cont_rect_Type1 : … … 899 896 let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 900 897  Kstop > h_Kstop 901  Kseq (x_ 7741, x_7740) >902 h_Kseq x_ 7741 x_7740898  Kseq (x_6057, x_6056) > 899 h_Kseq x_6057 x_6056 903 900 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 904 h_Kswitch h_Kcall x_ 7740)905  Kwhile (x_ 7744, x_7743, x_7742) >906 h_Kwhile x_ 7744 x_7743 x_7742901 h_Kswitch h_Kcall x_6056) 902  Kwhile (x_6060, x_6059, x_6058) > 903 h_Kwhile x_6060 x_6059 x_6058 907 904 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 908 h_Kswitch h_Kcall x_ 7742)909  Kdowhile (x_ 7747, x_7746, x_7745) >910 h_Kdowhile x_ 7747 x_7746 x_7745905 h_Kswitch h_Kcall x_6058) 906  Kdowhile (x_6063, x_6062, x_6061) > 907 h_Kdowhile x_6063 x_6062 x_6061 911 908 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 912 h_Kswitch h_Kcall x_ 7745)913  Kfor2 (x_ 7751, x_7750, x_7749, x_7748) >914 h_Kfor2 x_ 7751 x_7750 x_7749 x_7748909 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_6064 915 912 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 916 h_Kswitch h_Kcall x_ 7748)917  Kfor3 (x_ 7755, x_7754, x_7753, x_7752) >918 h_Kfor3 x_ 7755 x_7754 x_7753 x_7752913 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_6068 919 916 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 920 h_Kswitch h_Kcall x_ 7752)921  Kswitch x_ 7756>922 h_Kswitch x_ 7756917 h_Kswitch h_Kcall x_6068) 918  Kswitch x_6072 > 919 h_Kswitch x_6072 923 920 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 924 h_Kswitch h_Kcall x_ 7756)925  Kcall (x_ 7760, x_7759, x_7758, x_7757) >926 h_Kcall x_ 7760 x_7759 x_7758 x_7757921 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_6073 927 924 (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 928 h_Kswitch h_Kcall x_ 7757)925 h_Kswitch h_Kcall x_6073) 929 926 930 927 (** val cont_rect_Type0 : … … 939 936 let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function 940 937  Kstop > h_Kstop 941  Kseq (x_ 7771, x_7770) >942 h_Kseq x_ 7771 x_7770938  Kseq (x_6087, x_6086) > 939 h_Kseq x_6087 x_6086 943 940 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 944 h_Kswitch h_Kcall x_ 7770)945  Kwhile (x_ 7774, x_7773, x_7772) >946 h_Kwhile x_ 7774 x_7773 x_7772941 h_Kswitch h_Kcall x_6086) 942  Kwhile (x_6090, x_6089, x_6088) > 943 h_Kwhile x_6090 x_6089 x_6088 947 944 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 948 h_Kswitch h_Kcall x_ 7772)949  Kdowhile (x_ 7777, x_7776, x_7775) >950 h_Kdowhile x_ 7777 x_7776 x_7775945 h_Kswitch h_Kcall x_6088) 946  Kdowhile (x_6093, x_6092, x_6091) > 947 h_Kdowhile x_6093 x_6092 x_6091 951 948 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 952 h_Kswitch h_Kcall x_ 7775)953  Kfor2 (x_ 7781, x_7780, x_7779, x_7778) >954 h_Kfor2 x_ 7781 x_7780 x_7779 x_7778949 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_6094 955 952 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 956 h_Kswitch h_Kcall x_ 7778)957  Kfor3 (x_ 7785, x_7784, x_7783, x_7782) >958 h_Kfor3 x_ 7785 x_7784 x_7783 x_7782953 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_6098 959 956 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 960 h_Kswitch h_Kcall x_ 7782)961  Kswitch x_ 7786>962 h_Kswitch x_ 7786957 h_Kswitch h_Kcall x_6098) 958  Kswitch x_6102 > 959 h_Kswitch x_6102 963 960 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 964 h_Kswitch h_Kcall x_ 7786)965  Kcall (x_ 7790, x_7789, x_7788, x_7787) >966 h_Kcall x_ 7790 x_7789 x_7788 x_7787961 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_6103 967 964 (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 968 h_Kswitch h_Kcall x_ 7787)965 h_Kswitch h_Kcall x_6103) 969 966 970 967 (** val cont_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.