Changeset 1988 for src/joint


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

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

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEGlobalenvs.ma

    r1599 r1988  
    428428  λm,i_data,r.
    429429  let b ≝ mk_block r (nextblock … m) in
    430   〈mk_mem ? (update_block ? b
    431                  (mk_block_contents (mk_contentT beval BVundef) OZ i_data (λ_.BVundef))
     430  〈mk_mem (update_block ? b
     431                 (mk_block_contents OZ i_data (λ_.BVundef))
    432432                 (blocks … m))
    433433         (Zsucc (nextblock … m))
  • src/joint/BEMem.ma

    r1987 r1988  
    1515include "common/GenMem.ma".
    1616
    17 definition becontentT ≝ mk_contentT beval BVundef.
    18 definition bemem ≝ mem becontentT.
     17definition bemem ≝ mem.
    1918
    2019(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
    2120definition do_if_in_bounds:
    22  ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
     21 ∀A:Type[0]. bemem → pointer → (block → block_contents → Z → A) → option A ≝
    2322 λS,m,ptr,F.
    2423  let b ≝ pblock ptr in
     
    4039  (λb,content,off.
    4140    let contents ≝ update … off v (contents … content) in
    42     let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
     41    let content ≝ mk_block_contents (low … content) (high … content) contents in
    4342    let blocks ≝ update_block … b content (blocks … m) in
    4443     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
Note: See TracChangeset for help on using the changeset viewer.