Changeset 2933 for extracted/byteValues.ml
 Timestamp:
 Mar 21, 2013, 8:11:50 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/byteValues.ml
r2827 r2933 89 89 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 90 90 'a1 **) 91 let rec program_counter_rect_Type4 h_mk_program_counter x_ 6139=92 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6139in91 let rec program_counter_rect_Type4 h_mk_program_counter x_3 = 92 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_3 in 93 93 h_mk_program_counter pc_block0 pc_offset0 94 94 … … 96 96 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 97 97 'a1 **) 98 let rec program_counter_rect_Type5 h_mk_program_counter x_ 6141=99 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6141in98 let rec program_counter_rect_Type5 h_mk_program_counter x_5 = 99 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5 in 100 100 h_mk_program_counter pc_block0 pc_offset0 101 101 … … 103 103 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 104 104 'a1 **) 105 let rec program_counter_rect_Type3 h_mk_program_counter x_ 6143=106 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6143in105 let rec program_counter_rect_Type3 h_mk_program_counter x_7 = 106 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_7 in 107 107 h_mk_program_counter pc_block0 pc_offset0 108 108 … … 110 110 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 111 111 'a1 **) 112 let rec program_counter_rect_Type2 h_mk_program_counter x_ 6145=113 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6145in112 let rec program_counter_rect_Type2 h_mk_program_counter x_9 = 113 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_9 in 114 114 h_mk_program_counter pc_block0 pc_offset0 115 115 … … 117 117 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 118 118 'a1 **) 119 let rec program_counter_rect_Type1 h_mk_program_counter x_ 6147=120 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6147in119 let rec program_counter_rect_Type1 h_mk_program_counter x_11 = 120 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_11 in 121 121 h_mk_program_counter pc_block0 pc_offset0 122 122 … … 124 124 (Pointers.block Types.sig0 > Positive.pos > 'a1) > program_counter > 125 125 'a1 **) 126 let rec program_counter_rect_Type0 h_mk_program_counter x_ 6149=127 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_ 6149in126 let rec program_counter_rect_Type0 h_mk_program_counter x_13 = 127 let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_13 in 128 128 h_mk_program_counter pc_block0 pc_offset0 129 129 … … 215 215 216 216 (** val part_rect_Type4 : (Nat.nat > __ > 'a1) > part > 'a1 **) 217 let rec part_rect_Type4 h_mk_part x_ 6165=218 let part_no = x_ 6165in h_mk_part part_no __217 let rec part_rect_Type4 h_mk_part x_29 = 218 let part_no = x_29 in h_mk_part part_no __ 219 219 220 220 (** val part_rect_Type5 : (Nat.nat > __ > 'a1) > part > 'a1 **) 221 let rec part_rect_Type5 h_mk_part x_ 6167=222 let part_no = x_ 6167in h_mk_part part_no __221 let rec part_rect_Type5 h_mk_part x_31 = 222 let part_no = x_31 in h_mk_part part_no __ 223 223 224 224 (** val part_rect_Type3 : (Nat.nat > __ > 'a1) > part > 'a1 **) 225 let rec part_rect_Type3 h_mk_part x_ 6169=226 let part_no = x_ 6169in h_mk_part part_no __225 let rec part_rect_Type3 h_mk_part x_33 = 226 let part_no = x_33 in h_mk_part part_no __ 227 227 228 228 (** val part_rect_Type2 : (Nat.nat > __ > 'a1) > part > 'a1 **) 229 let rec part_rect_Type2 h_mk_part x_ 6171=230 let part_no = x_ 6171in h_mk_part part_no __229 let rec part_rect_Type2 h_mk_part x_35 = 230 let part_no = x_35 in h_mk_part part_no __ 231 231 232 232 (** val part_rect_Type1 : (Nat.nat > __ > 'a1) > part > 'a1 **) 233 let rec part_rect_Type1 h_mk_part x_ 6173=234 let part_no = x_ 6173in h_mk_part part_no __233 let rec part_rect_Type1 h_mk_part x_37 = 234 let part_no = x_37 in h_mk_part part_no __ 235 235 236 236 (** val part_rect_Type0 : (Nat.nat > __ > 'a1) > part > 'a1 **) 237 let rec part_rect_Type0 h_mk_part x_ 6175=238 let part_no = x_ 6175in h_mk_part part_no __237 let rec part_rect_Type0 h_mk_part x_39 = 238 let part_no = x_39 in h_mk_part part_no __ 239 239 240 240 (** val part_no : part > Nat.nat **) … … 486 486  BVundef > h_BVundef 487 487  BVnonzero > h_BVnonzero 488  BVXor (x_ 6209, x_6208, x_6207) > h_BVXor x_6209 x_6208 x_6207489  BVByte x_ 6210 > h_BVByte x_6210490  BVnull x_ 6211 > h_BVnull x_6211491  BVptr (x_ 6213, x_6212) > h_BVptr x_6213 x_6212492  BVpc (x_ 6215, x_6214) > h_BVpc x_6215 x_6214488  BVXor (x_73, x_72, x_71) > h_BVXor x_73 x_72 x_71 489  BVByte x_74 > h_BVByte x_74 490  BVnull x_75 > h_BVnull x_75 491  BVptr (x_77, x_76) > h_BVptr x_77 x_76 492  BVpc (x_79, x_78) > h_BVpc x_79 x_78 493 493 494 494 (** val beval_rect_Type5 : … … 500 500  BVundef > h_BVundef 501 501  BVnonzero > h_BVnonzero 502  BVXor (x_ 6226, x_6225, x_6224) > h_BVXor x_6226 x_6225 x_6224503  BVByte x_ 6227 > h_BVByte x_6227504  BVnull x_ 6228 > h_BVnull x_6228505  BVptr (x_ 6230, x_6229) > h_BVptr x_6230 x_6229506  BVpc (x_ 6232, x_6231) > h_BVpc x_6232 x_6231502  BVXor (x_90, x_89, x_88) > h_BVXor x_90 x_89 x_88 503  BVByte x_91 > h_BVByte x_91 504  BVnull x_92 > h_BVnull x_92 505  BVptr (x_94, x_93) > h_BVptr x_94 x_93 506  BVpc (x_96, x_95) > h_BVpc x_96 x_95 507 507 508 508 (** val beval_rect_Type3 : … … 514 514  BVundef > h_BVundef 515 515  BVnonzero > h_BVnonzero 516  BVXor (x_ 6243, x_6242, x_6241) > h_BVXor x_6243 x_6242 x_6241517  BVByte x_ 6244 > h_BVByte x_6244518  BVnull x_ 6245 > h_BVnull x_6245519  BVptr (x_ 6247, x_6246) > h_BVptr x_6247 x_6246520  BVpc (x_ 6249, x_6248) > h_BVpc x_6249 x_6248516  BVXor (x_107, x_106, x_105) > h_BVXor x_107 x_106 x_105 517  BVByte x_108 > h_BVByte x_108 518  BVnull x_109 > h_BVnull x_109 519  BVptr (x_111, x_110) > h_BVptr x_111 x_110 520  BVpc (x_113, x_112) > h_BVpc x_113 x_112 521 521 522 522 (** val beval_rect_Type2 : … … 528 528  BVundef > h_BVundef 529 529  BVnonzero > h_BVnonzero 530  BVXor (x_ 6260, x_6259, x_6258) > h_BVXor x_6260 x_6259 x_6258531  BVByte x_ 6261 > h_BVByte x_6261532  BVnull x_ 6262 > h_BVnull x_6262533  BVptr (x_ 6264, x_6263) > h_BVptr x_6264 x_6263534  BVpc (x_ 6266, x_6265) > h_BVpc x_6266 x_6265530  BVXor (x_124, x_123, x_122) > h_BVXor x_124 x_123 x_122 531  BVByte x_125 > h_BVByte x_125 532  BVnull x_126 > h_BVnull x_126 533  BVptr (x_128, x_127) > h_BVptr x_128 x_127 534  BVpc (x_130, x_129) > h_BVpc x_130 x_129 535 535 536 536 (** val beval_rect_Type1 : … … 542 542  BVundef > h_BVundef 543 543  BVnonzero > h_BVnonzero 544  BVXor (x_ 6277, x_6276, x_6275) > h_BVXor x_6277 x_6276 x_6275545  BVByte x_ 6278 > h_BVByte x_6278546  BVnull x_ 6279 > h_BVnull x_6279547  BVptr (x_ 6281, x_6280) > h_BVptr x_6281 x_6280548  BVpc (x_ 6283, x_6282) > h_BVpc x_6283 x_6282544  BVXor (x_141, x_140, x_139) > h_BVXor x_141 x_140 x_139 545  BVByte x_142 > h_BVByte x_142 546  BVnull x_143 > h_BVnull x_143 547  BVptr (x_145, x_144) > h_BVptr x_145 x_144 548  BVpc (x_147, x_146) > h_BVpc x_147 x_146 549 549 550 550 (** val beval_rect_Type0 : … … 556 556  BVundef > h_BVundef 557 557  BVnonzero > h_BVnonzero 558  BVXor (x_ 6294, x_6293, x_6292) > h_BVXor x_6294 x_6293 x_6292559  BVByte x_ 6295 > h_BVByte x_6295560  BVnull x_ 6296 > h_BVnull x_6296561  BVptr (x_ 6298, x_6297) > h_BVptr x_6298 x_6297562  BVpc (x_ 6300, x_6299) > h_BVpc x_6300 x_6299558  BVXor (x_158, x_157, x_156) > h_BVXor x_158 x_157 x_156 559  BVByte x_159 > h_BVByte x_159 560  BVnull x_160 > h_BVnull x_160 561  BVptr (x_162, x_161) > h_BVptr x_162 x_161 562  BVpc (x_164, x_163) > h_BVpc x_164 x_163 563 563 564 564 (** val beval_inv_rect_Type4 : … … 828 828  BVByte b > 829 829 Errors.OK 830 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 831 Nat.O)))))))) 832 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 833 Nat.O))))))))) b) 830 (Bool.notb 831 (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 832 (Nat.S Nat.O)))))))) 833 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 834 (Nat.S Nat.O))))))))) b)) 834 835  BVnull x > Errors.OK Bool.False 835 836  BVptr (x, x0) > Errors.OK Bool.True … … 890 891 ErrorMessages.NotAnInt32Val), List.Nil)))))))) 891 892 893 type add_or_sub = 894  Do_add 895  Do_sub 896 897 (** val add_or_sub_rect_Type4 : 'a1 > 'a1 > add_or_sub > 'a1 **) 898 let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function 899  Do_add > h_do_add 900  Do_sub > h_do_sub 901 902 (** val add_or_sub_rect_Type5 : 'a1 > 'a1 > add_or_sub > 'a1 **) 903 let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function 904  Do_add > h_do_add 905  Do_sub > h_do_sub 906 907 (** val add_or_sub_rect_Type3 : 'a1 > 'a1 > add_or_sub > 'a1 **) 908 let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function 909  Do_add > h_do_add 910  Do_sub > h_do_sub 911 912 (** val add_or_sub_rect_Type2 : 'a1 > 'a1 > add_or_sub > 'a1 **) 913 let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function 914  Do_add > h_do_add 915  Do_sub > h_do_sub 916 917 (** val add_or_sub_rect_Type1 : 'a1 > 'a1 > add_or_sub > 'a1 **) 918 let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function 919  Do_add > h_do_add 920  Do_sub > h_do_sub 921 922 (** val add_or_sub_rect_Type0 : 'a1 > 'a1 > add_or_sub > 'a1 **) 923 let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function 924  Do_add > h_do_add 925  Do_sub > h_do_sub 926 927 (** val add_or_sub_inv_rect_Type4 : 928 add_or_sub > (__ > 'a1) > (__ > 'a1) > 'a1 **) 929 let add_or_sub_inv_rect_Type4 hterm h1 h2 = 930 let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __ 931 932 (** val add_or_sub_inv_rect_Type3 : 933 add_or_sub > (__ > 'a1) > (__ > 'a1) > 'a1 **) 934 let add_or_sub_inv_rect_Type3 hterm h1 h2 = 935 let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __ 936 937 (** val add_or_sub_inv_rect_Type2 : 938 add_or_sub > (__ > 'a1) > (__ > 'a1) > 'a1 **) 939 let add_or_sub_inv_rect_Type2 hterm h1 h2 = 940 let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __ 941 942 (** val add_or_sub_inv_rect_Type1 : 943 add_or_sub > (__ > 'a1) > (__ > 'a1) > 'a1 **) 944 let add_or_sub_inv_rect_Type1 hterm h1 h2 = 945 let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __ 946 947 (** val add_or_sub_inv_rect_Type0 : 948 add_or_sub > (__ > 'a1) > (__ > 'a1) > 'a1 **) 949 let add_or_sub_inv_rect_Type0 hterm h1 h2 = 950 let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __ 951 952 (** val add_or_sub_discr : add_or_sub > add_or_sub > __ **) 953 let add_or_sub_discr x y = 954 Logic.eq_rect_Type2 x 955 (match x with 956  Do_add > Obj.magic (fun _ dH > dH) 957  Do_sub > Obj.magic (fun _ dH > dH)) y 958 959 (** val add_or_sub_jmdiscr : add_or_sub > add_or_sub > __ **) 960 let add_or_sub_jmdiscr x y = 961 Logic.eq_rect_Type2 x 962 (match x with 963  Do_add > Obj.magic (fun _ dH > dH) 964  Do_sub > Obj.magic (fun _ dH > dH)) y 965 966 (** val eq_add_or_sub : add_or_sub > add_or_sub > Bool.bool **) 967 let eq_add_or_sub x y = 968 match x with 969  Do_add > 970 (match y with 971  Do_add > Bool.True 972  Do_sub > Bool.False) 973  Do_sub > 974 (match y with 975  Do_add > Bool.False 976  Do_sub > Bool.True) 977 892 978 type bebit = 893 979  BBbit of Bool.bool 894 980  BBundef 895  BBptrcarry of Bool.bool* Pointers.pointer * part * BitVector.bitVector981  BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector 896 982 897 983 (** val bebit_rect_Type4 : 898 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >984 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 899 985 BitVector.bitVector > 'a1) > bebit > 'a1 **) 900 986 let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function 901  BBbit x_ 6419 > h_BBbit x_6419987  BBbit x_322 > h_BBbit x_322 902 988  BBundef > h_BBundef 903  BBptrcarry (x_6422, x_6421, p, x_6420) > 904 h_BBptrcarry x_6422 x_6421 p x_6420 989  BBptrcarry (x_325, x_324, p, x_323) > h_BBptrcarry x_325 x_324 p x_323 905 990 906 991 (** val bebit_rect_Type5 : 907 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >992 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 908 993 BitVector.bitVector > 'a1) > bebit > 'a1 **) 909 994 let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function 910  BBbit x_ 6427 > h_BBbit x_6427995  BBbit x_330 > h_BBbit x_330 911 996  BBundef > h_BBundef 912  BBptrcarry (x_6430, x_6429, p, x_6428) > 913 h_BBptrcarry x_6430 x_6429 p x_6428 997  BBptrcarry (x_333, x_332, p, x_331) > h_BBptrcarry x_333 x_332 p x_331 914 998 915 999 (** val bebit_rect_Type3 : 916 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >1000 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 917 1001 BitVector.bitVector > 'a1) > bebit > 'a1 **) 918 1002 let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function 919  BBbit x_ 6435 > h_BBbit x_64351003  BBbit x_338 > h_BBbit x_338 920 1004  BBundef > h_BBundef 921  BBptrcarry (x_6438, x_6437, p, x_6436) > 922 h_BBptrcarry x_6438 x_6437 p x_6436 1005  BBptrcarry (x_341, x_340, p, x_339) > h_BBptrcarry x_341 x_340 p x_339 923 1006 924 1007 (** val bebit_rect_Type2 : 925 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >1008 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 926 1009 BitVector.bitVector > 'a1) > bebit > 'a1 **) 927 1010 let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function 928  BBbit x_ 6443 > h_BBbit x_64431011  BBbit x_346 > h_BBbit x_346 929 1012  BBundef > h_BBundef 930  BBptrcarry (x_6446, x_6445, p, x_6444) > 931 h_BBptrcarry x_6446 x_6445 p x_6444 1013  BBptrcarry (x_349, x_348, p, x_347) > h_BBptrcarry x_349 x_348 p x_347 932 1014 933 1015 (** val bebit_rect_Type1 : 934 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >1016 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 935 1017 BitVector.bitVector > 'a1) > bebit > 'a1 **) 936 1018 let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function 937  BBbit x_ 6451 > h_BBbit x_64511019  BBbit x_354 > h_BBbit x_354 938 1020  BBundef > h_BBundef 939  BBptrcarry (x_6454, x_6453, p, x_6452) > 940 h_BBptrcarry x_6454 x_6453 p x_6452 1021  BBptrcarry (x_357, x_356, p, x_355) > h_BBptrcarry x_357 x_356 p x_355 941 1022 942 1023 (** val bebit_rect_Type0 : 943 (Bool.bool > 'a1) > 'a1 > ( Bool.bool> Pointers.pointer > part >1024 (Bool.bool > 'a1) > 'a1 > (add_or_sub > Pointers.pointer > part > 944 1025 BitVector.bitVector > 'a1) > bebit > 'a1 **) 945 1026 let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function 946  BBbit x_ 6459 > h_BBbit x_64591027  BBbit x_362 > h_BBbit x_362 947 1028  BBundef > h_BBundef 948  BBptrcarry (x_6462, x_6461, p, x_6460) > 949 h_BBptrcarry x_6462 x_6461 p x_6460 1029  BBptrcarry (x_365, x_364, p, x_363) > h_BBptrcarry x_365 x_364 p x_363 950 1030 951 1031 (** val bebit_inv_rect_Type4 : 952 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > ( Bool.bool>1032 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > (add_or_sub > 953 1033 Pointers.pointer > part > BitVector.bitVector > __ > 'a1) > 'a1 **) 954 1034 let bebit_inv_rect_Type4 hterm h1 h2 h3 = … … 956 1036 957 1037 (** val bebit_inv_rect_Type3 : 958 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > ( Bool.bool>1038 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > (add_or_sub > 959 1039 Pointers.pointer > part > BitVector.bitVector > __ > 'a1) > 'a1 **) 960 1040 let bebit_inv_rect_Type3 hterm h1 h2 h3 = … … 962 1042 963 1043 (** val bebit_inv_rect_Type2 : 964 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > ( Bool.bool>1044 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > (add_or_sub > 965 1045 Pointers.pointer > part > BitVector.bitVector > __ > 'a1) > 'a1 **) 966 1046 let bebit_inv_rect_Type2 hterm h1 h2 h3 = … … 968 1048 969 1049 (** val bebit_inv_rect_Type1 : 970 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > ( Bool.bool>1050 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > (add_or_sub > 971 1051 Pointers.pointer > part > BitVector.bitVector > __ > 'a1) > 'a1 **) 972 1052 let bebit_inv_rect_Type1 hterm h1 h2 h3 = … … 974 1054 975 1055 (** val bebit_inv_rect_Type0 : 976 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > ( Bool.bool>1056 bebit > (Bool.bool > __ > 'a1) > (__ > 'a1) > (add_or_sub > 977 1057 Pointers.pointer > part > BitVector.bitVector > __ > 'a1) > 'a1 **) 978 1058 let bebit_inv_rect_Type0 hterm h1 h2 h3 =
Note: See TracChangeset
for help on using the changeset viewer.