Changeset 1419


Ignore:
Timestamp:
Oct 19, 2011, 5:25:19 PM (8 years ago)
Author:
sacerdot
Message:

All axioms closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1395 r1419  
    1515include "common/GenMem.ma".
    1616
    17 definition bemem ≝ mem (mk_contentT beval BVundef).
     17definition becontentT ≝ mk_contentT beval BVundef.
     18definition bemem ≝ mem becontentT.
    1819
    19 axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
    20 axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.
     20(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
     21definition do_if_in_bounds:
     22 ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
     23 λS,m,ptr,F.
     24  let b ≝ pblock ptr in
     25  if Zltb (block_id b) (nextblock … m) then
     26   let content ≝ blocks … m b in
     27   let off ≝ offv (poff ptr) in
     28   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
     29    Some … (F b content off)
     30   else
     31    None ?
     32  else
     33   None ?.
     34
     35definition beloadv: ∀m:bemem. ∀ptr:pointer. option beval ≝
     36 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).
     37
     38definition bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem ≝
     39 λm,ptr,v. do_if_in_bounds … m ptr
     40  (λb,content,off.
     41    let contents ≝ update … off v (contents … content) in
     42    let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
     43    let blocks ≝ update_block … b content (blocks … m) in
     44     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).
    2145
    2246(* CSC: only pointers to XRAM or code memory ATM *)
Note: See TracChangeset for help on using the changeset viewer.