Changeset 635


Ignore:
Timestamp:
Mar 4, 2011, 6:20:21 PM (9 years ago)
Author:
campbell
Message:

Some commentary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Values.ma

    r583 r635  
    2424include "basics/logic.ma".
    2525
     26(* To define pointers we need a few details about the memory model.
     27
     28   There are several kinds of pointers, which differ in which regions of
     29   memory they address and the pointer's representation.
     30   
     31   Pointers are given as kind, block, offset triples, where a block identifies
     32   some memory in a given region with an arbitrary concrete address.  A proof
     33   is also required that the representation is suitable for the region the
     34   memory resides in.  Note that blocks cannot extend out of a region (in
     35   particular, a pdata pointer can address any byte in a pdata block - we never
     36   need to switch to a larger xdata pointer).
     37 *)
     38
     39(* blocks - represented by the region the memory resides in and a unique id *)
     40
    2641record block : Type[0] ≝
    2742{ block_region : region
     
    4459] qed.
    4560
    46 (* pointer_compat block_region pointer_region *)
     61(* Characterise the memory regions which the pointer representations can
     62   address.
     63
     64   pointer_compat <block> <pointer representation> *)
    4765
    4866inductive pointer_compat : block → region → Prop ≝
     
    5977definition is_pointer_compat : block → region → bool ≝
    6078λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     79
     80(* Offsets into the block.  We allow integers like CompCert so that we have
     81   the option of extending blocks backwards. *)
    6182
    6283record offset : Type[0] ≝ { offv : Z }.
Note: See TracChangeset for help on using the changeset viewer.