Changeset 3043 for extracted/pointers.ml


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/pointers.ml

    r3001 r3043  
    8080
    8181(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
    82 let rec block_rect_Type4 h_mk_block x_3896 =
    83   let block_id = x_3896 in h_mk_block block_id
     82let rec block_rect_Type4 h_mk_block x_5028 =
     83  let block_id = x_5028 in h_mk_block block_id
    8484
    8585(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
    86 let rec block_rect_Type5 h_mk_block x_3898 =
    87   let block_id = x_3898 in h_mk_block block_id
     86let rec block_rect_Type5 h_mk_block x_5030 =
     87  let block_id = x_5030 in h_mk_block block_id
    8888
    8989(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
    90 let rec block_rect_Type3 h_mk_block x_3900 =
    91   let block_id = x_3900 in h_mk_block block_id
     90let rec block_rect_Type3 h_mk_block x_5032 =
     91  let block_id = x_5032 in h_mk_block block_id
    9292
    9393(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
    94 let rec block_rect_Type2 h_mk_block x_3902 =
    95   let block_id = x_3902 in h_mk_block block_id
     94let rec block_rect_Type2 h_mk_block x_5034 =
     95  let block_id = x_5034 in h_mk_block block_id
    9696
    9797(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
    98 let rec block_rect_Type1 h_mk_block x_3904 =
    99   let block_id = x_3904 in h_mk_block block_id
     98let rec block_rect_Type1 h_mk_block x_5036 =
     99  let block_id = x_5036 in h_mk_block block_id
    100100
    101101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
    102 let rec block_rect_Type0 h_mk_block x_3906 =
    103   let block_id = x_3906 in h_mk_block block_id
     102let rec block_rect_Type0 h_mk_block x_5038 =
     103  let block_id = x_5038 in h_mk_block block_id
    104104
    105105(** val block_id : block -> Z.z **)
     
    163163
    164164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    165 let rec offset_rect_Type4 h_mk_offset x_3922 =
    166   let offv = x_3922 in h_mk_offset offv
     165let rec offset_rect_Type4 h_mk_offset x_5054 =
     166  let offv = x_5054 in h_mk_offset offv
    167167
    168168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    169 let rec offset_rect_Type5 h_mk_offset x_3924 =
    170   let offv = x_3924 in h_mk_offset offv
     169let rec offset_rect_Type5 h_mk_offset x_5056 =
     170  let offv = x_5056 in h_mk_offset offv
    171171
    172172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    173 let rec offset_rect_Type3 h_mk_offset x_3926 =
    174   let offv = x_3926 in h_mk_offset offv
     173let rec offset_rect_Type3 h_mk_offset x_5058 =
     174  let offv = x_5058 in h_mk_offset offv
    175175
    176176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    177 let rec offset_rect_Type2 h_mk_offset x_3928 =
    178   let offv = x_3928 in h_mk_offset offv
     177let rec offset_rect_Type2 h_mk_offset x_5060 =
     178  let offv = x_5060 in h_mk_offset offv
    179179
    180180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    181 let rec offset_rect_Type1 h_mk_offset x_3930 =
    182   let offv = x_3930 in h_mk_offset offv
     181let rec offset_rect_Type1 h_mk_offset x_5062 =
     182  let offv = x_5062 in h_mk_offset offv
    183183
    184184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    185 let rec offset_rect_Type0 h_mk_offset x_3932 =
    186   let offv = x_3932 in h_mk_offset offv
     185let rec offset_rect_Type0 h_mk_offset x_5064 =
     186  let offv = x_5064 in h_mk_offset offv
    187187
    188188(** val offv : offset -> BitVector.bitVector **)
     
    280280
    281281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    282 let rec pointer_rect_Type4 h_mk_pointer x_3948 =
    283   let { pblock = pblock; poff = poff } = x_3948 in
    284   h_mk_pointer pblock poff
     282let rec pointer_rect_Type4 h_mk_pointer x_5080 =
     283  let { pblock = pblock0; poff = poff0 } = x_5080 in
     284  h_mk_pointer pblock0 poff0
    285285
    286286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    287 let rec pointer_rect_Type5 h_mk_pointer x_3950 =
    288   let { pblock = pblock; poff = poff } = x_3950 in
    289   h_mk_pointer pblock poff
     287let rec pointer_rect_Type5 h_mk_pointer x_5082 =
     288  let { pblock = pblock0; poff = poff0 } = x_5082 in
     289  h_mk_pointer pblock0 poff0
    290290
    291291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    292 let rec pointer_rect_Type3 h_mk_pointer x_3952 =
    293   let { pblock = pblock; poff = poff } = x_3952 in
    294   h_mk_pointer pblock poff
     292let rec pointer_rect_Type3 h_mk_pointer x_5084 =
     293  let { pblock = pblock0; poff = poff0 } = x_5084 in
     294  h_mk_pointer pblock0 poff0
    295295
    296296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    297 let rec pointer_rect_Type2 h_mk_pointer x_3954 =
    298   let { pblock = pblock; poff = poff } = x_3954 in
    299   h_mk_pointer pblock poff
     297let rec pointer_rect_Type2 h_mk_pointer x_5086 =
     298  let { pblock = pblock0; poff = poff0 } = x_5086 in
     299  h_mk_pointer pblock0 poff0
    300300
    301301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    302 let rec pointer_rect_Type1 h_mk_pointer x_3956 =
    303   let { pblock = pblock; poff = poff } = x_3956 in
    304   h_mk_pointer pblock poff
     302let rec pointer_rect_Type1 h_mk_pointer x_5088 =
     303  let { pblock = pblock0; poff = poff0 } = x_5088 in
     304  h_mk_pointer pblock0 poff0
    305305
    306306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    307 let rec pointer_rect_Type0 h_mk_pointer x_3958 =
    308   let { pblock = pblock; poff = poff } = x_3958 in
    309   h_mk_pointer pblock poff
     307let rec pointer_rect_Type0 h_mk_pointer x_5090 =
     308  let { pblock = pblock0; poff = poff0 } = x_5090 in
     309  h_mk_pointer pblock0 poff0
    310310
    311311(** val pblock : pointer -> block **)
Note: See TracChangeset for help on using the changeset viewer.