Changeset 2797 for extracted/genMem.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (8 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/genMem.ml

    r2775 r2797  
    100100(** val block_contents_rect_Type4 :
    101101    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    102 let rec block_contents_rect_Type4 h_mk_block_contents x_6386 =
    103   let { low = low0; high = high0; contents = contents0 } = x_6386 in
     102let rec block_contents_rect_Type4 h_mk_block_contents x_6399 =
     103  let { low = low0; high = high0; contents = contents0 } = x_6399 in
    104104  h_mk_block_contents low0 high0 contents0
    105105
    106106(** val block_contents_rect_Type5 :
    107107    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    108 let rec block_contents_rect_Type5 h_mk_block_contents x_6388 =
    109   let { low = low0; high = high0; contents = contents0 } = x_6388 in
     108let rec block_contents_rect_Type5 h_mk_block_contents x_6401 =
     109  let { low = low0; high = high0; contents = contents0 } = x_6401 in
    110110  h_mk_block_contents low0 high0 contents0
    111111
    112112(** val block_contents_rect_Type3 :
    113113    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    114 let rec block_contents_rect_Type3 h_mk_block_contents x_6390 =
    115   let { low = low0; high = high0; contents = contents0 } = x_6390 in
     114let rec block_contents_rect_Type3 h_mk_block_contents x_6403 =
     115  let { low = low0; high = high0; contents = contents0 } = x_6403 in
    116116  h_mk_block_contents low0 high0 contents0
    117117
    118118(** val block_contents_rect_Type2 :
    119119    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    120 let rec block_contents_rect_Type2 h_mk_block_contents x_6392 =
    121   let { low = low0; high = high0; contents = contents0 } = x_6392 in
     120let rec block_contents_rect_Type2 h_mk_block_contents x_6405 =
     121  let { low = low0; high = high0; contents = contents0 } = x_6405 in
    122122  h_mk_block_contents low0 high0 contents0
    123123
    124124(** val block_contents_rect_Type1 :
    125125    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    126 let rec block_contents_rect_Type1 h_mk_block_contents x_6394 =
    127   let { low = low0; high = high0; contents = contents0 } = x_6394 in
     126let rec block_contents_rect_Type1 h_mk_block_contents x_6407 =
     127  let { low = low0; high = high0; contents = contents0 } = x_6407 in
    128128  h_mk_block_contents low0 high0 contents0
    129129
    130130(** val block_contents_rect_Type0 :
    131131    (Z.z -> Z.z -> contentmap -> 'a1) -> block_contents -> 'a1 **)
    132 let rec block_contents_rect_Type0 h_mk_block_contents x_6396 =
    133   let { low = low0; high = high0; contents = contents0 } = x_6396 in
     132let rec block_contents_rect_Type0 h_mk_block_contents x_6409 =
     133  let { low = low0; high = high0; contents = contents0 } = x_6409 in
    134134  h_mk_block_contents low0 high0 contents0
    135135
     
    187187(** val mem_rect_Type4 :
    188188    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    189 let rec mem_rect_Type4 h_mk_mem x_6412 =
    190   let { blocks = blocks0; nextblock = nextblock0 } = x_6412 in
     189let rec mem_rect_Type4 h_mk_mem x_6425 =
     190  let { blocks = blocks0; nextblock = nextblock0 } = x_6425 in
    191191  h_mk_mem blocks0 nextblock0 __
    192192
    193193(** val mem_rect_Type5 :
    194194    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    195 let rec mem_rect_Type5 h_mk_mem x_6414 =
    196   let { blocks = blocks0; nextblock = nextblock0 } = x_6414 in
     195let rec mem_rect_Type5 h_mk_mem x_6427 =
     196  let { blocks = blocks0; nextblock = nextblock0 } = x_6427 in
    197197  h_mk_mem blocks0 nextblock0 __
    198198
    199199(** val mem_rect_Type3 :
    200200    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    201 let rec mem_rect_Type3 h_mk_mem x_6416 =
    202   let { blocks = blocks0; nextblock = nextblock0 } = x_6416 in
     201let rec mem_rect_Type3 h_mk_mem x_6429 =
     202  let { blocks = blocks0; nextblock = nextblock0 } = x_6429 in
    203203  h_mk_mem blocks0 nextblock0 __
    204204
    205205(** val mem_rect_Type2 :
    206206    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    207 let rec mem_rect_Type2 h_mk_mem x_6418 =
    208   let { blocks = blocks0; nextblock = nextblock0 } = x_6418 in
     207let rec mem_rect_Type2 h_mk_mem x_6431 =
     208  let { blocks = blocks0; nextblock = nextblock0 } = x_6431 in
    209209  h_mk_mem blocks0 nextblock0 __
    210210
    211211(** val mem_rect_Type1 :
    212212    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    213 let rec mem_rect_Type1 h_mk_mem x_6420 =
    214   let { blocks = blocks0; nextblock = nextblock0 } = x_6420 in
     213let rec mem_rect_Type1 h_mk_mem x_6433 =
     214  let { blocks = blocks0; nextblock = nextblock0 } = x_6433 in
    215215  h_mk_mem blocks0 nextblock0 __
    216216
    217217(** val mem_rect_Type0 :
    218218    ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1 **)
    219 let rec mem_rect_Type0 h_mk_mem x_6422 =
    220   let { blocks = blocks0; nextblock = nextblock0 } = x_6422 in
     219let rec mem_rect_Type0 h_mk_mem x_6435 =
     220  let { blocks = blocks0; nextblock = nextblock0 } = x_6435 in
    221221  h_mk_mem blocks0 nextblock0 __
    222222
Note: See TracChangeset for help on using the changeset viewer.