Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2775 r2797  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6009 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6009 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6022 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6022 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_6011 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6011 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6024 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6024 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_6013 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6013 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6026 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6026 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_6015 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6015 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6028 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6028 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_6017 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6017 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6030 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6030 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_6019 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6019 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6032 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6032 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_6035 =
    218   let part_no = x_6035 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6048 =
     218  let part_no = x_6048 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_6037 =
    222   let part_no = x_6037 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6050 =
     222  let part_no = x_6050 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_6039 =
    226   let part_no = x_6039 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6052 =
     226  let part_no = x_6052 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_6041 =
    230   let part_no = x_6041 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6054 =
     230  let part_no = x_6054 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_6043 =
    234   let part_no = x_6043 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6056 =
     234  let part_no = x_6056 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_6045 =
    238   let part_no = x_6045 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6058 =
     238  let part_no = x_6058 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_6079, x_6078, x_6077) -> h_BVXor x_6079 x_6078 x_6077
    489 | BVByte x_6080 -> h_BVByte x_6080
    490 | BVnull x_6081 -> h_BVnull x_6081
    491 | BVptr (x_6083, x_6082) -> h_BVptr x_6083 x_6082
    492 | BVpc (x_6085, x_6084) -> h_BVpc x_6085 x_6084
     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
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_6096, x_6095, x_6094) -> h_BVXor x_6096 x_6095 x_6094
    503 | BVByte x_6097 -> h_BVByte x_6097
    504 | BVnull x_6098 -> h_BVnull x_6098
    505 | BVptr (x_6100, x_6099) -> h_BVptr x_6100 x_6099
    506 | BVpc (x_6102, x_6101) -> h_BVpc x_6102 x_6101
     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
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_6113, x_6112, x_6111) -> h_BVXor x_6113 x_6112 x_6111
    517 | BVByte x_6114 -> h_BVByte x_6114
    518 | BVnull x_6115 -> h_BVnull x_6115
    519 | BVptr (x_6117, x_6116) -> h_BVptr x_6117 x_6116
    520 | BVpc (x_6119, x_6118) -> h_BVpc x_6119 x_6118
     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
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_6130, x_6129, x_6128) -> h_BVXor x_6130 x_6129 x_6128
    531 | BVByte x_6131 -> h_BVByte x_6131
    532 | BVnull x_6132 -> h_BVnull x_6132
    533 | BVptr (x_6134, x_6133) -> h_BVptr x_6134 x_6133
    534 | BVpc (x_6136, x_6135) -> h_BVpc x_6136 x_6135
     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
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_6147, x_6146, x_6145) -> h_BVXor x_6147 x_6146 x_6145
    545 | BVByte x_6148 -> h_BVByte x_6148
    546 | BVnull x_6149 -> h_BVnull x_6149
    547 | BVptr (x_6151, x_6150) -> h_BVptr x_6151 x_6150
    548 | BVpc (x_6153, x_6152) -> h_BVpc x_6153 x_6152
     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
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_6164, x_6163, x_6162) -> h_BVXor x_6164 x_6163 x_6162
    559 | BVByte x_6165 -> h_BVByte x_6165
    560 | BVnull x_6166 -> h_BVnull x_6166
    561 | BVptr (x_6168, x_6167) -> h_BVptr x_6168 x_6167
    562 | BVpc (x_6170, x_6169) -> h_BVpc x_6170 x_6169
     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
    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_6289 -> h_BBbit x_6289
     901| BBbit x_6302 -> h_BBbit x_6302
    902902| BBundef -> h_BBundef
    903 | BBptrcarry (x_6292, x_6291, p, x_6290) ->
    904   h_BBptrcarry x_6292 x_6291 p x_6290
     903| BBptrcarry (x_6305, x_6304, p, x_6303) ->
     904  h_BBptrcarry x_6305 x_6304 p x_6303
    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_6297 -> h_BBbit x_6297
     910| BBbit x_6310 -> h_BBbit x_6310
    911911| BBundef -> h_BBundef
    912 | BBptrcarry (x_6300, x_6299, p, x_6298) ->
    913   h_BBptrcarry x_6300 x_6299 p x_6298
     912| BBptrcarry (x_6313, x_6312, p, x_6311) ->
     913  h_BBptrcarry x_6313 x_6312 p x_6311
    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_6305 -> h_BBbit x_6305
     919| BBbit x_6318 -> h_BBbit x_6318
    920920| BBundef -> h_BBundef
    921 | BBptrcarry (x_6308, x_6307, p, x_6306) ->
    922   h_BBptrcarry x_6308 x_6307 p x_6306
     921| BBptrcarry (x_6321, x_6320, p, x_6319) ->
     922  h_BBptrcarry x_6321 x_6320 p x_6319
    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_6313 -> h_BBbit x_6313
     928| BBbit x_6326 -> h_BBbit x_6326
    929929| BBundef -> h_BBundef
    930 | BBptrcarry (x_6316, x_6315, p, x_6314) ->
    931   h_BBptrcarry x_6316 x_6315 p x_6314
     930| BBptrcarry (x_6329, x_6328, p, x_6327) ->
     931  h_BBptrcarry x_6329 x_6328 p x_6327
    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_6321 -> h_BBbit x_6321
     937| BBbit x_6334 -> h_BBbit x_6334
    938938| BBundef -> h_BBundef
    939 | BBptrcarry (x_6324, x_6323, p, x_6322) ->
    940   h_BBptrcarry x_6324 x_6323 p x_6322
     939| BBptrcarry (x_6337, x_6336, p, x_6335) ->
     940  h_BBptrcarry x_6337 x_6336 p x_6335
    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_6329 -> h_BBbit x_6329
     946| BBbit x_6342 -> h_BBbit x_6342
    947947| BBundef -> h_BBundef
    948 | BBptrcarry (x_6332, x_6331, p, x_6330) ->
    949   h_BBptrcarry x_6332 x_6331 p x_6330
     948| BBptrcarry (x_6345, x_6344, p, x_6343) ->
     949  h_BBptrcarry x_6345 x_6344 p x_6343
    950950
    951951(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.