Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (7 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2797 r2827  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6022 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6022 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6139 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6139 in
    9393  h_mk_program_counter pc_block0 pc_offset0
    9494
     
    9696    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9797    'a1 **)
    98 let rec program_counter_rect_Type5 h_mk_program_counter x_6024 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6024 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6141 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6141 in
    100100  h_mk_program_counter pc_block0 pc_offset0
    101101
     
    103103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    104104    'a1 **)
    105 let rec program_counter_rect_Type3 h_mk_program_counter x_6026 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6026 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6143 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6143 in
    107107  h_mk_program_counter pc_block0 pc_offset0
    108108
     
    110110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    111111    'a1 **)
    112 let rec program_counter_rect_Type2 h_mk_program_counter x_6028 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6028 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6145 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6145 in
    114114  h_mk_program_counter pc_block0 pc_offset0
    115115
     
    117117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    118118    'a1 **)
    119 let rec program_counter_rect_Type1 h_mk_program_counter x_6030 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6030 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6147 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6147 in
    121121  h_mk_program_counter pc_block0 pc_offset0
    122122
     
    124124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    125125    'a1 **)
    126 let rec program_counter_rect_Type0 h_mk_program_counter x_6032 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6032 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6149 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6149 in
    128128  h_mk_program_counter pc_block0 pc_offset0
    129129
     
    215215
    216216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    217 let rec part_rect_Type4 h_mk_part x_6048 =
    218   let part_no = x_6048 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6165 =
     218  let part_no = x_6165 in h_mk_part part_no __
    219219
    220220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    221 let rec part_rect_Type5 h_mk_part x_6050 =
    222   let part_no = x_6050 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6167 =
     222  let part_no = x_6167 in h_mk_part part_no __
    223223
    224224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    225 let rec part_rect_Type3 h_mk_part x_6052 =
    226   let part_no = x_6052 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6169 =
     226  let part_no = x_6169 in h_mk_part part_no __
    227227
    228228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    229 let rec part_rect_Type2 h_mk_part x_6054 =
    230   let part_no = x_6054 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6171 =
     230  let part_no = x_6171 in h_mk_part part_no __
    231231
    232232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    233 let rec part_rect_Type1 h_mk_part x_6056 =
    234   let part_no = x_6056 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6173 =
     234  let part_no = x_6173 in h_mk_part part_no __
    235235
    236236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    237 let rec part_rect_Type0 h_mk_part x_6058 =
    238   let part_no = x_6058 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6175 =
     238  let part_no = x_6175 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    486486| BVundef -> h_BVundef
    487487| BVnonzero -> h_BVnonzero
    488 | BVXor (x_6092, x_6091, x_6090) -> h_BVXor x_6092 x_6091 x_6090
    489 | BVByte x_6093 -> h_BVByte x_6093
    490 | BVnull x_6094 -> h_BVnull x_6094
    491 | BVptr (x_6096, x_6095) -> h_BVptr x_6096 x_6095
    492 | BVpc (x_6098, x_6097) -> h_BVpc x_6098 x_6097
     488| BVXor (x_6209, x_6208, x_6207) -> h_BVXor x_6209 x_6208 x_6207
     489| BVByte x_6210 -> h_BVByte x_6210
     490| BVnull x_6211 -> h_BVnull x_6211
     491| BVptr (x_6213, x_6212) -> h_BVptr x_6213 x_6212
     492| BVpc (x_6215, x_6214) -> h_BVpc x_6215 x_6214
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_6109, x_6108, x_6107) -> h_BVXor x_6109 x_6108 x_6107
    503 | BVByte x_6110 -> h_BVByte x_6110
    504 | BVnull x_6111 -> h_BVnull x_6111
    505 | BVptr (x_6113, x_6112) -> h_BVptr x_6113 x_6112
    506 | BVpc (x_6115, x_6114) -> h_BVpc x_6115 x_6114
     502| BVXor (x_6226, x_6225, x_6224) -> h_BVXor x_6226 x_6225 x_6224
     503| BVByte x_6227 -> h_BVByte x_6227
     504| BVnull x_6228 -> h_BVnull x_6228
     505| BVptr (x_6230, x_6229) -> h_BVptr x_6230 x_6229
     506| BVpc (x_6232, x_6231) -> h_BVpc x_6232 x_6231
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_6126, x_6125, x_6124) -> h_BVXor x_6126 x_6125 x_6124
    517 | BVByte x_6127 -> h_BVByte x_6127
    518 | BVnull x_6128 -> h_BVnull x_6128
    519 | BVptr (x_6130, x_6129) -> h_BVptr x_6130 x_6129
    520 | BVpc (x_6132, x_6131) -> h_BVpc x_6132 x_6131
     516| BVXor (x_6243, x_6242, x_6241) -> h_BVXor x_6243 x_6242 x_6241
     517| BVByte x_6244 -> h_BVByte x_6244
     518| BVnull x_6245 -> h_BVnull x_6245
     519| BVptr (x_6247, x_6246) -> h_BVptr x_6247 x_6246
     520| BVpc (x_6249, x_6248) -> h_BVpc x_6249 x_6248
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_6143, x_6142, x_6141) -> h_BVXor x_6143 x_6142 x_6141
    531 | BVByte x_6144 -> h_BVByte x_6144
    532 | BVnull x_6145 -> h_BVnull x_6145
    533 | BVptr (x_6147, x_6146) -> h_BVptr x_6147 x_6146
    534 | BVpc (x_6149, x_6148) -> h_BVpc x_6149 x_6148
     530| BVXor (x_6260, x_6259, x_6258) -> h_BVXor x_6260 x_6259 x_6258
     531| BVByte x_6261 -> h_BVByte x_6261
     532| BVnull x_6262 -> h_BVnull x_6262
     533| BVptr (x_6264, x_6263) -> h_BVptr x_6264 x_6263
     534| BVpc (x_6266, x_6265) -> h_BVpc x_6266 x_6265
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_6160, x_6159, x_6158) -> h_BVXor x_6160 x_6159 x_6158
    545 | BVByte x_6161 -> h_BVByte x_6161
    546 | BVnull x_6162 -> h_BVnull x_6162
    547 | BVptr (x_6164, x_6163) -> h_BVptr x_6164 x_6163
    548 | BVpc (x_6166, x_6165) -> h_BVpc x_6166 x_6165
     544| BVXor (x_6277, x_6276, x_6275) -> h_BVXor x_6277 x_6276 x_6275
     545| BVByte x_6278 -> h_BVByte x_6278
     546| BVnull x_6279 -> h_BVnull x_6279
     547| BVptr (x_6281, x_6280) -> h_BVptr x_6281 x_6280
     548| BVpc (x_6283, x_6282) -> h_BVpc x_6283 x_6282
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_6177, x_6176, x_6175) -> h_BVXor x_6177 x_6176 x_6175
    559 | BVByte x_6178 -> h_BVByte x_6178
    560 | BVnull x_6179 -> h_BVnull x_6179
    561 | BVptr (x_6181, x_6180) -> h_BVptr x_6181 x_6180
    562 | BVpc (x_6183, x_6182) -> h_BVpc x_6183 x_6182
     558| BVXor (x_6294, x_6293, x_6292) -> h_BVXor x_6294 x_6293 x_6292
     559| BVByte x_6295 -> h_BVByte x_6295
     560| BVnull x_6296 -> h_BVnull x_6296
     561| BVptr (x_6298, x_6297) -> h_BVptr x_6298 x_6297
     562| BVpc (x_6300, x_6299) -> h_BVpc x_6300 x_6299
    563563
    564564(** val beval_inv_rect_Type4 :
     
    899899    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    900900let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    901 | BBbit x_6302 -> h_BBbit x_6302
     901| BBbit x_6419 -> h_BBbit x_6419
    902902| BBundef -> h_BBundef
    903 | BBptrcarry (x_6305, x_6304, p, x_6303) ->
    904   h_BBptrcarry x_6305 x_6304 p x_6303
     903| BBptrcarry (x_6422, x_6421, p, x_6420) ->
     904  h_BBptrcarry x_6422 x_6421 p x_6420
    905905
    906906(** val bebit_rect_Type5 :
     
    908908    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    909909let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    910 | BBbit x_6310 -> h_BBbit x_6310
     910| BBbit x_6427 -> h_BBbit x_6427
    911911| BBundef -> h_BBundef
    912 | BBptrcarry (x_6313, x_6312, p, x_6311) ->
    913   h_BBptrcarry x_6313 x_6312 p x_6311
     912| BBptrcarry (x_6430, x_6429, p, x_6428) ->
     913  h_BBptrcarry x_6430 x_6429 p x_6428
    914914
    915915(** val bebit_rect_Type3 :
     
    917917    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    918918let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    919 | BBbit x_6318 -> h_BBbit x_6318
     919| BBbit x_6435 -> h_BBbit x_6435
    920920| BBundef -> h_BBundef
    921 | BBptrcarry (x_6321, x_6320, p, x_6319) ->
    922   h_BBptrcarry x_6321 x_6320 p x_6319
     921| BBptrcarry (x_6438, x_6437, p, x_6436) ->
     922  h_BBptrcarry x_6438 x_6437 p x_6436
    923923
    924924(** val bebit_rect_Type2 :
     
    926926    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    927927let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    928 | BBbit x_6326 -> h_BBbit x_6326
     928| BBbit x_6443 -> h_BBbit x_6443
    929929| BBundef -> h_BBundef
    930 | BBptrcarry (x_6329, x_6328, p, x_6327) ->
    931   h_BBptrcarry x_6329 x_6328 p x_6327
     930| BBptrcarry (x_6446, x_6445, p, x_6444) ->
     931  h_BBptrcarry x_6446 x_6445 p x_6444
    932932
    933933(** val bebit_rect_Type1 :
     
    935935    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    936936let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    937 | BBbit x_6334 -> h_BBbit x_6334
     937| BBbit x_6451 -> h_BBbit x_6451
    938938| BBundef -> h_BBundef
    939 | BBptrcarry (x_6337, x_6336, p, x_6335) ->
    940   h_BBptrcarry x_6337 x_6336 p x_6335
     939| BBptrcarry (x_6454, x_6453, p, x_6452) ->
     940  h_BBptrcarry x_6454 x_6453 p x_6452
    941941
    942942(** val bebit_rect_Type0 :
     
    944944    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    945945let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    946 | BBbit x_6342 -> h_BBbit x_6342
     946| BBbit x_6459 -> h_BBbit x_6459
    947947| BBundef -> h_BBundef
    948 | BBptrcarry (x_6345, x_6344, p, x_6343) ->
    949   h_BBptrcarry x_6345 x_6344 p x_6343
     948| BBptrcarry (x_6462, x_6461, p, x_6460) ->
     949  h_BBptrcarry x_6462 x_6461 p x_6460
    950950
    951951(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.