Changeset 2797 for extracted/pointers.ml


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

    r2775 r2797  
    8080
    8181(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
    82 let rec block_rect_Type4 h_mk_block x_4885 =
    83   let block_id = x_4885 in h_mk_block block_id
     82let rec block_rect_Type4 h_mk_block x_4898 =
     83  let block_id = x_4898 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_4887 =
    87   let block_id = x_4887 in h_mk_block block_id
     86let rec block_rect_Type5 h_mk_block x_4900 =
     87  let block_id = x_4900 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_4889 =
    91   let block_id = x_4889 in h_mk_block block_id
     90let rec block_rect_Type3 h_mk_block x_4902 =
     91  let block_id = x_4902 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_4891 =
    95   let block_id = x_4891 in h_mk_block block_id
     94let rec block_rect_Type2 h_mk_block x_4904 =
     95  let block_id = x_4904 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_4893 =
    99   let block_id = x_4893 in h_mk_block block_id
     98let rec block_rect_Type1 h_mk_block x_4906 =
     99  let block_id = x_4906 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_4895 =
    103   let block_id = x_4895 in h_mk_block block_id
     102let rec block_rect_Type0 h_mk_block x_4908 =
     103  let block_id = x_4908 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_4911 =
    166   let offv = x_4911 in h_mk_offset offv
     165let rec offset_rect_Type4 h_mk_offset x_4924 =
     166  let offv = x_4924 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_4913 =
    170   let offv = x_4913 in h_mk_offset offv
     169let rec offset_rect_Type5 h_mk_offset x_4926 =
     170  let offv = x_4926 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_4915 =
    174   let offv = x_4915 in h_mk_offset offv
     173let rec offset_rect_Type3 h_mk_offset x_4928 =
     174  let offv = x_4928 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_4917 =
    178   let offv = x_4917 in h_mk_offset offv
     177let rec offset_rect_Type2 h_mk_offset x_4930 =
     178  let offv = x_4930 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_4919 =
    182   let offv = x_4919 in h_mk_offset offv
     181let rec offset_rect_Type1 h_mk_offset x_4932 =
     182  let offv = x_4932 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_4921 =
    186   let offv = x_4921 in h_mk_offset offv
     185let rec offset_rect_Type0 h_mk_offset x_4934 =
     186  let offv = x_4934 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_4937 =
    283   let { pblock = pblock0; poff = poff0 } = x_4937 in
     282let rec pointer_rect_Type4 h_mk_pointer x_4950 =
     283  let { pblock = pblock0; poff = poff0 } = x_4950 in
    284284  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_4939 =
    288   let { pblock = pblock0; poff = poff0 } = x_4939 in
     287let rec pointer_rect_Type5 h_mk_pointer x_4952 =
     288  let { pblock = pblock0; poff = poff0 } = x_4952 in
    289289  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_4941 =
    293   let { pblock = pblock0; poff = poff0 } = x_4941 in
     292let rec pointer_rect_Type3 h_mk_pointer x_4954 =
     293  let { pblock = pblock0; poff = poff0 } = x_4954 in
    294294  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_4943 =
    298   let { pblock = pblock0; poff = poff0 } = x_4943 in
     297let rec pointer_rect_Type2 h_mk_pointer x_4956 =
     298  let { pblock = pblock0; poff = poff0 } = x_4956 in
    299299  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_4945 =
    303   let { pblock = pblock0; poff = poff0 } = x_4945 in
     302let rec pointer_rect_Type1 h_mk_pointer x_4958 =
     303  let { pblock = pblock0; poff = poff0 } = x_4958 in
    304304  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_4947 =
    308   let { pblock = pblock0; poff = poff0 } = x_4947 in
     307let rec pointer_rect_Type0 h_mk_pointer x_4960 =
     308  let { pblock = pblock0; poff = poff0 } = x_4960 in
    309309  h_mk_pointer pblock0 poff0
    310310
Note: See TracChangeset for help on using the changeset viewer.