Changeset 127 for C-semantics/Csem.ma


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

Allow the storage of pointers in suitably large integers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r125 r127  
    401401
    402402ninductive type_pointable : type → Prop ≝
    403 | type_ptr_int : type_pointable (Tint I32 Unsigned)
     403          (* All integer sizes can represent at least one kind of pointer *)
     404| type_ptr_int : ∀sz. type_pointable (Tint sz Unsigned)
    404405| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
    405406| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     
    407408
    408409ninductive type_space : type → memory_space → Prop ≝
    409 | type_spc_int : type_space (Tint I32 Unsigned) Any
     410| type_spc_int : ∀s,sz. sizeof_pointer s ≤ sizeof (Tint sz Unsigned) →
     411                           type_space (Tint sz Unsigned) s
    410412| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    411413| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    431433      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
    432434  | cast_pp_z: ∀m,ty,ty'.
    433       type_pointable ty → (* Don't care which space it is for the source type *)
     435      type_pointable ty →
    434436      type_pointable ty' →
    435437      cast m (Vint zero) ty ty' (Vint zero).
    436 (* XXX: other integers?
    437   | cast_nn_i: ∀m,n,t1,t2.     (**r no change in data representation *)
    438       neutral_for_cast t1 → neutral_for_cast t2 →
     438(* Perhaps a little too generous?  For example, some integers may not
     439   represent a valid generic pointer.
     440  | cast_pp_i: ∀m,n,ty,ty',t1,t2.     (**r no change in data representation *)
     441      type_pointable ty →
     442      type_pointable ty' →
     443      sizeof ty ≤ sizeof ty' →
    439444      cast m (Vint n) t1 t2 (Vint n).
    440445*)
     446
    441447(* * * Operational semantics *)
    442448
Note: See TracChangeset for help on using the changeset viewer.