Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (7 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1986 r1988  
    7979     addresses of the memory region in question - here there are no real
    8080     pointers, so use the real region. *)
    81   let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in
     81  let ptr ≝ mk_pointer (block_region m b) b ? (mk_offset p) in
    8282  match id with
    8383  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    151151definition alloc_init_data : mem → list init_data → region → mem × block ≝
    152152  λm,i_data,r.
    153   let b ≝ mk_block r (nextblock ? m) in
    154   〈mk_mem ? (update_block ? b
    155                  (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef))
    156                  (blocks ? m))
    157          (Zsucc (nextblock ? m))
    158          (succ_nextblock_pos ? m),
     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),
    159159   b〉.
    160160
     
    198198λF,V,init_info,p.
    199199  add_globals … init_info
    200    〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?
     200   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem
    201201   (prog_vars ?? p).
    202202
Note: See TracChangeset for help on using the changeset viewer.