Changeset 2951 for extracted/genMem.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/genMem.ml

    r2827 r2951  
    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_6516 =
    103   let { low = low0; high = high0; contents = contents0 } = x_6516 in
     102let rec block_contents_rect_Type4 h_mk_block_contents x_6555 =
     103  let { low = low0; high = high0; contents = contents0 } = x_6555 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_6518 =
    109   let { low = low0; high = high0; contents = contents0 } = x_6518 in
     108let rec block_contents_rect_Type5 h_mk_block_contents x_6557 =
     109  let { low = low0; high = high0; contents = contents0 } = x_6557 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_6520 =
    115   let { low = low0; high = high0; contents = contents0 } = x_6520 in
     114let rec block_contents_rect_Type3 h_mk_block_contents x_6559 =
     115  let { low = low0; high = high0; contents = contents0 } = x_6559 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_6522 =
    121   let { low = low0; high = high0; contents = contents0 } = x_6522 in
     120let rec block_contents_rect_Type2 h_mk_block_contents x_6561 =
     121  let { low = low0; high = high0; contents = contents0 } = x_6561 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_6524 =
    127   let { low = low0; high = high0; contents = contents0 } = x_6524 in
     126let rec block_contents_rect_Type1 h_mk_block_contents x_6563 =
     127  let { low = low0; high = high0; contents = contents0 } = x_6563 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_6526 =
    133   let { low = low0; high = high0; contents = contents0 } = x_6526 in
     132let rec block_contents_rect_Type0 h_mk_block_contents x_6565 =
     133  let { low = low0; high = high0; contents = contents0 } = x_6565 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_6542 =
    190   let { blocks = blocks0; nextblock = nextblock0 } = x_6542 in
     189let rec mem_rect_Type4 h_mk_mem x_6581 =
     190  let { blocks = blocks0; nextblock = nextblock0 } = x_6581 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_6544 =
    196   let { blocks = blocks0; nextblock = nextblock0 } = x_6544 in
     195let rec mem_rect_Type5 h_mk_mem x_6583 =
     196  let { blocks = blocks0; nextblock = nextblock0 } = x_6583 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_6546 =
    202   let { blocks = blocks0; nextblock = nextblock0 } = x_6546 in
     201let rec mem_rect_Type3 h_mk_mem x_6585 =
     202  let { blocks = blocks0; nextblock = nextblock0 } = x_6585 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_6548 =
    208   let { blocks = blocks0; nextblock = nextblock0 } = x_6548 in
     207let rec mem_rect_Type2 h_mk_mem x_6587 =
     208  let { blocks = blocks0; nextblock = nextblock0 } = x_6587 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_6550 =
    214   let { blocks = blocks0; nextblock = nextblock0 } = x_6550 in
     213let rec mem_rect_Type1 h_mk_mem x_6589 =
     214  let { blocks = blocks0; nextblock = nextblock0 } = x_6589 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_6552 =
    220   let { blocks = blocks0; nextblock = nextblock0 } = x_6552 in
     219let rec mem_rect_Type0 h_mk_mem x_6591 =
     220  let { blocks = blocks0; nextblock = nextblock0 } = x_6591 in
    221221  h_mk_mem blocks0 nextblock0 __
    222222
Note: See TracChangeset for help on using the changeset viewer.