Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2717 r2730  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6074 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6074 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_5700 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5700 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_6076 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6076 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_5702 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5702 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_6078 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6078 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_5704 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5704 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_6080 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6080 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_5706 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5706 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_6082 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6082 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_5708 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5708 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_6084 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6084 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_5710 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5710 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_6100 =
    218   let part_no = x_6100 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_5726 =
     218  let part_no = x_5726 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_6102 =
    222   let part_no = x_6102 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_5728 =
     222  let part_no = x_5728 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_6104 =
    226   let part_no = x_6104 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_5730 =
     226  let part_no = x_5730 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_6106 =
    230   let part_no = x_6106 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_5732 =
     230  let part_no = x_5732 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_6108 =
    234   let part_no = x_6108 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_5734 =
     234  let part_no = x_5734 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_6110 =
    238   let part_no = x_6110 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_5736 =
     238  let part_no = x_5736 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    326326| BVundef -> h_BVundef
    327327| BVnonzero -> h_BVnonzero
    328 | BVXor (x_6144, x_6143, x_6142) -> h_BVXor x_6144 x_6143 x_6142
    329 | BVByte x_6145 -> h_BVByte x_6145
    330 | BVnull x_6146 -> h_BVnull x_6146
    331 | BVptr (x_6148, x_6147) -> h_BVptr x_6148 x_6147
    332 | BVpc (x_6150, x_6149) -> h_BVpc x_6150 x_6149
     328| BVXor (x_5770, x_5769, x_5768) -> h_BVXor x_5770 x_5769 x_5768
     329| BVByte x_5771 -> h_BVByte x_5771
     330| BVnull x_5772 -> h_BVnull x_5772
     331| BVptr (x_5774, x_5773) -> h_BVptr x_5774 x_5773
     332| BVpc (x_5776, x_5775) -> h_BVpc x_5776 x_5775
    333333
    334334(** val beval_rect_Type5 :
     
    340340| BVundef -> h_BVundef
    341341| BVnonzero -> h_BVnonzero
    342 | BVXor (x_6161, x_6160, x_6159) -> h_BVXor x_6161 x_6160 x_6159
    343 | BVByte x_6162 -> h_BVByte x_6162
    344 | BVnull x_6163 -> h_BVnull x_6163
    345 | BVptr (x_6165, x_6164) -> h_BVptr x_6165 x_6164
    346 | BVpc (x_6167, x_6166) -> h_BVpc x_6167 x_6166
     342| BVXor (x_5787, x_5786, x_5785) -> h_BVXor x_5787 x_5786 x_5785
     343| BVByte x_5788 -> h_BVByte x_5788
     344| BVnull x_5789 -> h_BVnull x_5789
     345| BVptr (x_5791, x_5790) -> h_BVptr x_5791 x_5790
     346| BVpc (x_5793, x_5792) -> h_BVpc x_5793 x_5792
    347347
    348348(** val beval_rect_Type3 :
     
    354354| BVundef -> h_BVundef
    355355| BVnonzero -> h_BVnonzero
    356 | BVXor (x_6178, x_6177, x_6176) -> h_BVXor x_6178 x_6177 x_6176
    357 | BVByte x_6179 -> h_BVByte x_6179
    358 | BVnull x_6180 -> h_BVnull x_6180
    359 | BVptr (x_6182, x_6181) -> h_BVptr x_6182 x_6181
    360 | BVpc (x_6184, x_6183) -> h_BVpc x_6184 x_6183
     356| BVXor (x_5804, x_5803, x_5802) -> h_BVXor x_5804 x_5803 x_5802
     357| BVByte x_5805 -> h_BVByte x_5805
     358| BVnull x_5806 -> h_BVnull x_5806
     359| BVptr (x_5808, x_5807) -> h_BVptr x_5808 x_5807
     360| BVpc (x_5810, x_5809) -> h_BVpc x_5810 x_5809
    361361
    362362(** val beval_rect_Type2 :
     
    368368| BVundef -> h_BVundef
    369369| BVnonzero -> h_BVnonzero
    370 | BVXor (x_6195, x_6194, x_6193) -> h_BVXor x_6195 x_6194 x_6193
    371 | BVByte x_6196 -> h_BVByte x_6196
    372 | BVnull x_6197 -> h_BVnull x_6197
    373 | BVptr (x_6199, x_6198) -> h_BVptr x_6199 x_6198
    374 | BVpc (x_6201, x_6200) -> h_BVpc x_6201 x_6200
     370| BVXor (x_5821, x_5820, x_5819) -> h_BVXor x_5821 x_5820 x_5819
     371| BVByte x_5822 -> h_BVByte x_5822
     372| BVnull x_5823 -> h_BVnull x_5823
     373| BVptr (x_5825, x_5824) -> h_BVptr x_5825 x_5824
     374| BVpc (x_5827, x_5826) -> h_BVpc x_5827 x_5826
    375375
    376376(** val beval_rect_Type1 :
     
    382382| BVundef -> h_BVundef
    383383| BVnonzero -> h_BVnonzero
    384 | BVXor (x_6212, x_6211, x_6210) -> h_BVXor x_6212 x_6211 x_6210
    385 | BVByte x_6213 -> h_BVByte x_6213
    386 | BVnull x_6214 -> h_BVnull x_6214
    387 | BVptr (x_6216, x_6215) -> h_BVptr x_6216 x_6215
    388 | BVpc (x_6218, x_6217) -> h_BVpc x_6218 x_6217
     384| BVXor (x_5838, x_5837, x_5836) -> h_BVXor x_5838 x_5837 x_5836
     385| BVByte x_5839 -> h_BVByte x_5839
     386| BVnull x_5840 -> h_BVnull x_5840
     387| BVptr (x_5842, x_5841) -> h_BVptr x_5842 x_5841
     388| BVpc (x_5844, x_5843) -> h_BVpc x_5844 x_5843
    389389
    390390(** val beval_rect_Type0 :
     
    396396| BVundef -> h_BVundef
    397397| BVnonzero -> h_BVnonzero
    398 | BVXor (x_6229, x_6228, x_6227) -> h_BVXor x_6229 x_6228 x_6227
    399 | BVByte x_6230 -> h_BVByte x_6230
    400 | BVnull x_6231 -> h_BVnull x_6231
    401 | BVptr (x_6233, x_6232) -> h_BVptr x_6233 x_6232
    402 | BVpc (x_6235, x_6234) -> h_BVpc x_6235 x_6234
     398| BVXor (x_5855, x_5854, x_5853) -> h_BVXor x_5855 x_5854 x_5853
     399| BVByte x_5856 -> h_BVByte x_5856
     400| BVnull x_5857 -> h_BVnull x_5857
     401| BVptr (x_5859, x_5858) -> h_BVptr x_5859 x_5858
     402| BVpc (x_5861, x_5860) -> h_BVpc x_5861 x_5860
    403403
    404404(** val beval_inv_rect_Type4 :
     
    739739    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    740740let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    741 | BBbit x_6354 -> h_BBbit x_6354
     741| BBbit x_5980 -> h_BBbit x_5980
    742742| BBundef -> h_BBundef
    743 | BBptrcarry (x_6357, x_6356, p, x_6355) ->
    744   h_BBptrcarry x_6357 x_6356 p x_6355
     743| BBptrcarry (x_5983, x_5982, p, x_5981) ->
     744  h_BBptrcarry x_5983 x_5982 p x_5981
    745745
    746746(** val bebit_rect_Type5 :
     
    748748    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    749749let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    750 | BBbit x_6362 -> h_BBbit x_6362
     750| BBbit x_5988 -> h_BBbit x_5988
    751751| BBundef -> h_BBundef
    752 | BBptrcarry (x_6365, x_6364, p, x_6363) ->
    753   h_BBptrcarry x_6365 x_6364 p x_6363
     752| BBptrcarry (x_5991, x_5990, p, x_5989) ->
     753  h_BBptrcarry x_5991 x_5990 p x_5989
    754754
    755755(** val bebit_rect_Type3 :
     
    757757    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    758758let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    759 | BBbit x_6370 -> h_BBbit x_6370
     759| BBbit x_5996 -> h_BBbit x_5996
    760760| BBundef -> h_BBundef
    761 | BBptrcarry (x_6373, x_6372, p, x_6371) ->
    762   h_BBptrcarry x_6373 x_6372 p x_6371
     761| BBptrcarry (x_5999, x_5998, p, x_5997) ->
     762  h_BBptrcarry x_5999 x_5998 p x_5997
    763763
    764764(** val bebit_rect_Type2 :
     
    766766    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    767767let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    768 | BBbit x_6378 -> h_BBbit x_6378
     768| BBbit x_6004 -> h_BBbit x_6004
    769769| BBundef -> h_BBundef
    770 | BBptrcarry (x_6381, x_6380, p, x_6379) ->
    771   h_BBptrcarry x_6381 x_6380 p x_6379
     770| BBptrcarry (x_6007, x_6006, p, x_6005) ->
     771  h_BBptrcarry x_6007 x_6006 p x_6005
    772772
    773773(** val bebit_rect_Type1 :
     
    775775    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    776776let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    777 | BBbit x_6386 -> h_BBbit x_6386
     777| BBbit x_6012 -> h_BBbit x_6012
    778778| BBundef -> h_BBundef
    779 | BBptrcarry (x_6389, x_6388, p, x_6387) ->
    780   h_BBptrcarry x_6389 x_6388 p x_6387
     779| BBptrcarry (x_6015, x_6014, p, x_6013) ->
     780  h_BBptrcarry x_6015 x_6014 p x_6013
    781781
    782782(** val bebit_rect_Type0 :
     
    784784    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    785785let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    786 | BBbit x_6394 -> h_BBbit x_6394
     786| BBbit x_6020 -> h_BBbit x_6020
    787787| BBundef -> h_BBundef
    788 | BBptrcarry (x_6397, x_6396, p, x_6395) ->
    789   h_BBptrcarry x_6397 x_6396 p x_6395
     788| BBptrcarry (x_6023, x_6022, p, x_6021) ->
     789  h_BBptrcarry x_6023 x_6022 p x_6021
    790790
    791791(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.