Changeset 1994


Ignore:
Timestamp:
May 24, 2012, 6:08:02 PM (5 years ago)
Author:
campbell
Message:

Remove redundant allocation definition in Globalenvs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1993 r1994  
    148148*)
    149149
    150 (* TODO: why doesn't this use alloc? *)
    151 definition alloc_init_data : mem → list init_data → region → mem × block ≝
    152   λm,i_data,r.
    153   let b ≝ mk_block r (nextblock m) in
    154   〈mk_mem (update_block ? b
    155                  (mk_block_contents OZ (size_init_data_list i_data) (λ_.BVundef))
    156                  (blocks m))
    157          (Zsucc (nextblock m))
    158          (succ_nextblock_pos m),
    159    b〉.
    160150
    161151(* init *)
     
    173163      let init ≝ extract_init init_info in
    174164      let 〈g,st〉 ≝ g_st in
    175         let 〈st',b〉 ≝ alloc_init_data st init r in
     165        let 〈st',b〉 ≝ alloc st OZ (size_init_data_list init) r in
    176166          let g' ≝ add_symbol ? id b g in
    177167            〈g', st'〉
Note: See TracChangeset for help on using the changeset viewer.