Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2773 r2775  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_4404 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4404 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6009 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6009 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_4406 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4406 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6011 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6011 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_4408 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4408 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6013 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6013 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_4410 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4410 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6015 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6015 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_4412 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4412 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6017 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6017 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_4414 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4414 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6019 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6019 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_4430 =
    218   let part_no = x_4430 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6035 =
     218  let part_no = x_6035 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_4432 =
    222   let part_no = x_4432 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6037 =
     222  let part_no = x_6037 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_4434 =
    226   let part_no = x_4434 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6039 =
     226  let part_no = x_6039 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_4436 =
    230   let part_no = x_4436 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6041 =
     230  let part_no = x_6041 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_4438 =
    234   let part_no = x_4438 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6043 =
     234  let part_no = x_6043 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_4440 =
    238   let part_no = x_4440 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6045 =
     238  let part_no = x_6045 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_4474, x_4473, x_4472) -> h_BVXor x_4474 x_4473 x_4472
    489 | BVByte x_4475 -> h_BVByte x_4475
    490 | BVnull x_4476 -> h_BVnull x_4476
    491 | BVptr (x_4478, x_4477) -> h_BVptr x_4478 x_4477
    492 | BVpc (x_4480, x_4479) -> h_BVpc x_4480 x_4479
     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
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_4491, x_4490, x_4489) -> h_BVXor x_4491 x_4490 x_4489
    503 | BVByte x_4492 -> h_BVByte x_4492
    504 | BVnull x_4493 -> h_BVnull x_4493
    505 | BVptr (x_4495, x_4494) -> h_BVptr x_4495 x_4494
    506 | BVpc (x_4497, x_4496) -> h_BVpc x_4497 x_4496
     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
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_4508, x_4507, x_4506) -> h_BVXor x_4508 x_4507 x_4506
    517 | BVByte x_4509 -> h_BVByte x_4509
    518 | BVnull x_4510 -> h_BVnull x_4510
    519 | BVptr (x_4512, x_4511) -> h_BVptr x_4512 x_4511
    520 | BVpc (x_4514, x_4513) -> h_BVpc x_4514 x_4513
     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
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_4525, x_4524, x_4523) -> h_BVXor x_4525 x_4524 x_4523
    531 | BVByte x_4526 -> h_BVByte x_4526
    532 | BVnull x_4527 -> h_BVnull x_4527
    533 | BVptr (x_4529, x_4528) -> h_BVptr x_4529 x_4528
    534 | BVpc (x_4531, x_4530) -> h_BVpc x_4531 x_4530
     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
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_4542, x_4541, x_4540) -> h_BVXor x_4542 x_4541 x_4540
    545 | BVByte x_4543 -> h_BVByte x_4543
    546 | BVnull x_4544 -> h_BVnull x_4544
    547 | BVptr (x_4546, x_4545) -> h_BVptr x_4546 x_4545
    548 | BVpc (x_4548, x_4547) -> h_BVpc x_4548 x_4547
     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
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_4559, x_4558, x_4557) -> h_BVXor x_4559 x_4558 x_4557
    559 | BVByte x_4560 -> h_BVByte x_4560
    560 | BVnull x_4561 -> h_BVnull x_4561
    561 | BVptr (x_4563, x_4562) -> h_BVptr x_4563 x_4562
    562 | BVpc (x_4565, x_4564) -> h_BVpc x_4565 x_4564
     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
    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_4684 -> h_BBbit x_4684
     901| BBbit x_6289 -> h_BBbit x_6289
    902902| BBundef -> h_BBundef
    903 | BBptrcarry (x_4687, x_4686, p, x_4685) ->
    904   h_BBptrcarry x_4687 x_4686 p x_4685
     903| BBptrcarry (x_6292, x_6291, p, x_6290) ->
     904  h_BBptrcarry x_6292 x_6291 p x_6290
    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_4692 -> h_BBbit x_4692
     910| BBbit x_6297 -> h_BBbit x_6297
    911911| BBundef -> h_BBundef
    912 | BBptrcarry (x_4695, x_4694, p, x_4693) ->
    913   h_BBptrcarry x_4695 x_4694 p x_4693
     912| BBptrcarry (x_6300, x_6299, p, x_6298) ->
     913  h_BBptrcarry x_6300 x_6299 p x_6298
    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_4700 -> h_BBbit x_4700
     919| BBbit x_6305 -> h_BBbit x_6305
    920920| BBundef -> h_BBundef
    921 | BBptrcarry (x_4703, x_4702, p, x_4701) ->
    922   h_BBptrcarry x_4703 x_4702 p x_4701
     921| BBptrcarry (x_6308, x_6307, p, x_6306) ->
     922  h_BBptrcarry x_6308 x_6307 p x_6306
    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_4708 -> h_BBbit x_4708
     928| BBbit x_6313 -> h_BBbit x_6313
    929929| BBundef -> h_BBundef
    930 | BBptrcarry (x_4711, x_4710, p, x_4709) ->
    931   h_BBptrcarry x_4711 x_4710 p x_4709
     930| BBptrcarry (x_6316, x_6315, p, x_6314) ->
     931  h_BBptrcarry x_6316 x_6315 p x_6314
    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_4716 -> h_BBbit x_4716
     937| BBbit x_6321 -> h_BBbit x_6321
    938938| BBundef -> h_BBundef
    939 | BBptrcarry (x_4719, x_4718, p, x_4717) ->
    940   h_BBptrcarry x_4719 x_4718 p x_4717
     939| BBptrcarry (x_6324, x_6323, p, x_6322) ->
     940  h_BBptrcarry x_6324 x_6323 p x_6322
    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_4724 -> h_BBbit x_4724
     946| BBbit x_6329 -> h_BBbit x_6329
    947947| BBundef -> h_BBundef
    948 | BBptrcarry (x_4727, x_4726, p, x_4725) ->
    949   h_BBptrcarry x_4727 x_4726 p x_4725
     948| BBptrcarry (x_6332, x_6331, p, x_6330) ->
     949  h_BBptrcarry x_6332 x_6331 p x_6330
    950950
    951951(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.