Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r3001 r3043  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_2980 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2980 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6152 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6152 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_2982 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2982 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6154 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6154 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_2984 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2984 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6156 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6156 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_2986 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2986 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6158 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6158 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_2988 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2988 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6160 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6160 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_2990 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_2990 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6162 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6162 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_3006 =
    218   let part_no = x_3006 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6178 =
     218  let part_no = x_6178 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_3008 =
    222   let part_no = x_3008 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6180 =
     222  let part_no = x_6180 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_3010 =
    226   let part_no = x_3010 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6182 =
     226  let part_no = x_6182 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_3012 =
    230   let part_no = x_3012 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6184 =
     230  let part_no = x_6184 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_3014 =
    234   let part_no = x_3014 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6186 =
     234  let part_no = x_6186 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_3016 =
    238   let part_no = x_3016 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6188 =
     238  let part_no = x_6188 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_3050, x_3049, x_3048) -> h_BVXor x_3050 x_3049 x_3048
    489 | BVByte x_3051 -> h_BVByte x_3051
    490 | BVnull x_3052 -> h_BVnull x_3052
    491 | BVptr (x_3054, x_3053) -> h_BVptr x_3054 x_3053
    492 | BVpc (x_3056, x_3055) -> h_BVpc x_3056 x_3055
     488| BVXor (x_6222, x_6221, x_6220) -> h_BVXor x_6222 x_6221 x_6220
     489| BVByte x_6223 -> h_BVByte x_6223
     490| BVnull x_6224 -> h_BVnull x_6224
     491| BVptr (x_6226, x_6225) -> h_BVptr x_6226 x_6225
     492| BVpc (x_6228, x_6227) -> h_BVpc x_6228 x_6227
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_3067, x_3066, x_3065) -> h_BVXor x_3067 x_3066 x_3065
    503 | BVByte x_3068 -> h_BVByte x_3068
    504 | BVnull x_3069 -> h_BVnull x_3069
    505 | BVptr (x_3071, x_3070) -> h_BVptr x_3071 x_3070
    506 | BVpc (x_3073, x_3072) -> h_BVpc x_3073 x_3072
     502| BVXor (x_6239, x_6238, x_6237) -> h_BVXor x_6239 x_6238 x_6237
     503| BVByte x_6240 -> h_BVByte x_6240
     504| BVnull x_6241 -> h_BVnull x_6241
     505| BVptr (x_6243, x_6242) -> h_BVptr x_6243 x_6242
     506| BVpc (x_6245, x_6244) -> h_BVpc x_6245 x_6244
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_3084, x_3083, x_3082) -> h_BVXor x_3084 x_3083 x_3082
    517 | BVByte x_3085 -> h_BVByte x_3085
    518 | BVnull x_3086 -> h_BVnull x_3086
    519 | BVptr (x_3088, x_3087) -> h_BVptr x_3088 x_3087
    520 | BVpc (x_3090, x_3089) -> h_BVpc x_3090 x_3089
     516| BVXor (x_6256, x_6255, x_6254) -> h_BVXor x_6256 x_6255 x_6254
     517| BVByte x_6257 -> h_BVByte x_6257
     518| BVnull x_6258 -> h_BVnull x_6258
     519| BVptr (x_6260, x_6259) -> h_BVptr x_6260 x_6259
     520| BVpc (x_6262, x_6261) -> h_BVpc x_6262 x_6261
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_3101, x_3100, x_3099) -> h_BVXor x_3101 x_3100 x_3099
    531 | BVByte x_3102 -> h_BVByte x_3102
    532 | BVnull x_3103 -> h_BVnull x_3103
    533 | BVptr (x_3105, x_3104) -> h_BVptr x_3105 x_3104
    534 | BVpc (x_3107, x_3106) -> h_BVpc x_3107 x_3106
     530| BVXor (x_6273, x_6272, x_6271) -> h_BVXor x_6273 x_6272 x_6271
     531| BVByte x_6274 -> h_BVByte x_6274
     532| BVnull x_6275 -> h_BVnull x_6275
     533| BVptr (x_6277, x_6276) -> h_BVptr x_6277 x_6276
     534| BVpc (x_6279, x_6278) -> h_BVpc x_6279 x_6278
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_3118, x_3117, x_3116) -> h_BVXor x_3118 x_3117 x_3116
    545 | BVByte x_3119 -> h_BVByte x_3119
    546 | BVnull x_3120 -> h_BVnull x_3120
    547 | BVptr (x_3122, x_3121) -> h_BVptr x_3122 x_3121
    548 | BVpc (x_3124, x_3123) -> h_BVpc x_3124 x_3123
     544| BVXor (x_6290, x_6289, x_6288) -> h_BVXor x_6290 x_6289 x_6288
     545| BVByte x_6291 -> h_BVByte x_6291
     546| BVnull x_6292 -> h_BVnull x_6292
     547| BVptr (x_6294, x_6293) -> h_BVptr x_6294 x_6293
     548| BVpc (x_6296, x_6295) -> h_BVpc x_6296 x_6295
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_3135, x_3134, x_3133) -> h_BVXor x_3135 x_3134 x_3133
    559 | BVByte x_3136 -> h_BVByte x_3136
    560 | BVnull x_3137 -> h_BVnull x_3137
    561 | BVptr (x_3139, x_3138) -> h_BVptr x_3139 x_3138
    562 | BVpc (x_3141, x_3140) -> h_BVpc x_3141 x_3140
     558| BVXor (x_6307, x_6306, x_6305) -> h_BVXor x_6307 x_6306 x_6305
     559| BVByte x_6308 -> h_BVByte x_6308
     560| BVnull x_6309 -> h_BVnull x_6309
     561| BVptr (x_6311, x_6310) -> h_BVptr x_6311 x_6310
     562| BVpc (x_6313, x_6312) -> h_BVpc x_6313 x_6312
    563563
    564564(** val beval_inv_rect_Type4 :
     
    685685                         (Bool.andb (Nat.eqb (part_no p1) Nat.O)
    686686                           (Nat.eqb (part_no p2) (Nat.S Nat.O)))
    687                          (Pointers.eq_block (Pointers.pblock ptr1)
    688                            (Pointers.pblock ptr2)))
     687                         (Pointers.eq_block ptr1.Pointers.pblock
     688                           ptr2.Pointers.pblock))
    689689                       (eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    690690                         (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S
     
    692692                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    693693                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
    694                          (Pointers.offv (Pointers.poff ptr1))
    695                          (Pointers.offv (Pointers.poff ptr2))) with
     694                         (Pointers.offv ptr1.Pointers.poff)
     695                         (Pointers.offv ptr2.Pointers.poff)) with
    696696               | Bool.True ->
    697697                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
     
    985985    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    986986let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    987 | BBbit x_3299 -> h_BBbit x_3299
     987| BBbit x_6471 -> h_BBbit x_6471
    988988| BBundef -> h_BBundef
    989 | BBptrcarry (x_3302, x_3301, p, x_3300) ->
    990   h_BBptrcarry x_3302 x_3301 p x_3300
     989| BBptrcarry (x_6474, x_6473, p, x_6472) ->
     990  h_BBptrcarry x_6474 x_6473 p x_6472
    991991
    992992(** val bebit_rect_Type5 :
     
    994994    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    995995let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    996 | BBbit x_3307 -> h_BBbit x_3307
     996| BBbit x_6479 -> h_BBbit x_6479
    997997| BBundef -> h_BBundef
    998 | BBptrcarry (x_3310, x_3309, p, x_3308) ->
    999   h_BBptrcarry x_3310 x_3309 p x_3308
     998| BBptrcarry (x_6482, x_6481, p, x_6480) ->
     999  h_BBptrcarry x_6482 x_6481 p x_6480
    10001000
    10011001(** val bebit_rect_Type3 :
     
    10031003    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    10041004let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    1005 | BBbit x_3315 -> h_BBbit x_3315
     1005| BBbit x_6487 -> h_BBbit x_6487
    10061006| BBundef -> h_BBundef
    1007 | BBptrcarry (x_3318, x_3317, p, x_3316) ->
    1008   h_BBptrcarry x_3318 x_3317 p x_3316
     1007| BBptrcarry (x_6490, x_6489, p, x_6488) ->
     1008  h_BBptrcarry x_6490 x_6489 p x_6488
    10091009
    10101010(** val bebit_rect_Type2 :
     
    10121012    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    10131013let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    1014 | BBbit x_3323 -> h_BBbit x_3323
     1014| BBbit x_6495 -> h_BBbit x_6495
    10151015| BBundef -> h_BBundef
    1016 | BBptrcarry (x_3326, x_3325, p, x_3324) ->
    1017   h_BBptrcarry x_3326 x_3325 p x_3324
     1016| BBptrcarry (x_6498, x_6497, p, x_6496) ->
     1017  h_BBptrcarry x_6498 x_6497 p x_6496
    10181018
    10191019(** val bebit_rect_Type1 :
     
    10211021    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    10221022let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    1023 | BBbit x_3331 -> h_BBbit x_3331
     1023| BBbit x_6503 -> h_BBbit x_6503
    10241024| BBundef -> h_BBundef
    1025 | BBptrcarry (x_3334, x_3333, p, x_3332) ->
    1026   h_BBptrcarry x_3334 x_3333 p x_3332
     1025| BBptrcarry (x_6506, x_6505, p, x_6504) ->
     1026  h_BBptrcarry x_6506 x_6505 p x_6504
    10271027
    10281028(** val bebit_rect_Type0 :
     
    10301030    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    10311031let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    1032 | BBbit x_3339 -> h_BBbit x_3339
     1032| BBbit x_6511 -> h_BBbit x_6511
    10331033| BBundef -> h_BBundef
    1034 | BBptrcarry (x_3342, x_3341, p, x_3340) ->
    1035   h_BBptrcarry x_3342 x_3341 p x_3340
     1034| BBptrcarry (x_6514, x_6513, p, x_6512) ->
     1035  h_BBptrcarry x_6514 x_6513 p x_6512
    10361036
    10371037(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.