Changeset 125 for C-semantics/Values.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Values.ma

    r124 r125  
    3636*)
    3737
    38 ninductive ptr_class : Type ≝
    39 | Universal : ptr_class
    40 | Data : ptr_class
    41 | IData : ptr_class
    42 | XData : ptr_class
    43 (* pdata?  I'd rather not... *)
    44 | Code : ptr_class.
    45 
    46 ninductive ptr_class_compat : ptr_class → ptr_class → Prop ≝
    47 | ptr_class_same : ∀pcl. ptr_class_compat pcl pcl
    48 | ptr_univ_l : ∀pcl. ptr_class_compat Universal pcl
    49 | ptr_univ_r : ∀pcl. ptr_class_compat pcl Universal.
    50 
    51 nlemma ptr_class_compat_sym : ∀p,p'. ptr_class_compat p p' → ptr_class_compat p' p.
    52 #p p' H; ninversion H; //; nqed.
    53 
    5438(* TODO: should comparison and subtraction of pointers of different sorts
    5539         be supported? *)
     
    5943  | Vint: int -> val
    6044  | Vfloat: float -> val
    61   | Vptr: ptr_class → block -> int -> val.
     45  | Vptr: memory_space → block -> int -> val.
    6246
    6347ndefinition Vzero: val ≝ Vint zero.
Note: See TracChangeset for help on using the changeset viewer.