Changeset 155 for C-semantics/Csem.ma


Ignore:
Timestamp:
Oct 6, 2010, 2:20:30 PM (9 years ago)
Author:
campbell
Message:

More sensible handling of integer types and pointer casts.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r127 r155  
    402402ninductive type_pointable : type → Prop ≝
    403403          (* All integer sizes can represent at least one kind of pointer *)
    404 | type_ptr_int : ∀sz. type_pointable (Tint sz Unsigned)
    405404| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
    406405| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     
    408407
    409408ninductive type_space : type → memory_space → Prop ≝
    410 | type_spc_int : ∀s,sz. sizeof_pointer s ≤ sizeof (Tint sz Unsigned) →
    411                            type_space (Tint sz Unsigned) s
    412409| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    413410| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     411(* XXX Is the following necessary? *)
    414412| type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code.
    415413
     
    428426           (Vfloat (cast_float_float sz2 f))
    429427  | cast_pp: ∀m,psp,psp',ty,ty',b,ofs.
    430       type_pointable ty
     428      type_space ty psp
    431429      type_space ty' psp' →
    432430      pointer_compat (block_space m b) psp' →
    433431      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
     432  | cast_ip_z: ∀m,sz,sg,ty'.
     433      type_pointable ty' →
     434      cast m (Vint zero) (Tint sz sg) ty' (Vint zero)
    434435  | cast_pp_z: ∀m,ty,ty'.
    435436      type_pointable ty →
    436437      type_pointable ty' →
    437438      cast m (Vint zero) ty ty' (Vint zero).
     439(* Should probably also allow pointers to pass through sufficiently large
     440   unsigned integers. *)
    438441(* Perhaps a little too generous?  For example, some integers may not
    439442   represent a valid generic pointer.
Note: See TracChangeset for help on using the changeset viewer.