Changeset 1988 for src/common/Mem.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/common/Mem.ma

    r1874 r1988  
    22include "common/FrontEndVal.ma".
    33
    4 definition mem ≝ bemem.
    5 
    6 let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
     4let rec loadn (m:mem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
    75match n with
    86[ O ⇒ Some ? ([ ])
     
    2321  ].
    2422
    25 let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝
     23let rec loadv (t:typ) (m:mem) (addr:val) on addr : option val ≝
    2624match addr with
    2725[ Vptr ptr ⇒ load t m ptr
     
    2927].
    3028
    31 let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝
     29let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option mem ≝
    3230match vs with
    3331[ nil ⇒ Some ? m
     
    3937].
    4038
    41 definition store : typ → bemem → pointer → val → option bemem ≝
     39definition store : typ → bemem → pointer → val → option mem ≝
    4240λt,m,ptr,v. storen m ptr (fe_to_be_values t v).
    4341
    44 definition storev : typ → bemem → val → val → option bemem ≝
     42definition storev : typ → bemem → val → val → option mem ≝
    4543λt,m,addr,v.
    4644  match addr with
     
    5250
    5351definition valid_pointer : mem → pointer → bool ≝
    54 λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧
    55   Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧
    56   Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)).
     52λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
     53  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
     54  Zleb (offv (poff ptr)) (high_bound m (pblock ptr)).
    5755
    5856
Note: See TracChangeset for help on using the changeset viewer.