Changeset 1988 for src/joint/BEMem.ma


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/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.