From fa7415be2fe9b240374f0a51c1cd4a9de5376c5a Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 6 Sep 2006 20:00:02 +0000 Subject: Permettre les casts entre types de fonction git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a76dcb4..5431697 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -335,6 +335,16 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. +Inductive neutral_for_cast: type -> Prop := + | nfc_int: forall sg, + neutral_for_cast (Tint I32 sg) + | nfc_ptr: forall ty, + neutral_for_cast (Tpointer ty) + | nfc_array: forall ty sz, + neutral_for_cast (Tarray ty sz) + | nfc_fun: forall targs tres, + neutral_for_cast (Tfunction targs tres). + Inductive cast : val -> type -> type -> val -> Prop := | cast_ii: forall i sz2 sz1 si1 si2, cast (Vint i) (Tint sz1 si1) (Tint sz2 si2) @@ -348,18 +358,12 @@ Inductive cast : val -> type -> type -> val -> Prop := | cast_ff: forall f sz1 sz2, cast (Vfloat f) (Tfloat sz1) (Tfloat sz2) (Vfloat (cast_float_float sz2 f)) - | cast_ip_p: forall b ofs t1 si2, - cast (Vptr b ofs) (Tint I32 si2) (Tpointer t1) (Vptr b ofs) - | cast_pi_p: forall b ofs t1 si2, - cast (Vptr b ofs) (Tpointer t1) (Tint I32 si2) (Vptr b ofs) - | cast_pp_p: forall b ofs t1 t2, - cast (Vptr b ofs) (Tpointer t1) (Tpointer t2) (Vptr b ofs) - | cast_ip_i: forall n t1 si2, - cast (Vint n) (Tint I32 si2) (Tpointer t1) (Vint n) - | cast_pi_i: forall n t1 si2, - cast (Vint n) (Tpointer t1) (Tint I32 si2) (Vint n) - | cast_pp_i: forall n t1 t2, - cast (Vint n) (Tpointer t1) (Tpointer t2) (Vint n). + | cast_nn_p: forall b ofs t1 t2, + neutral_for_cast t1 -> neutral_for_cast t2 -> + cast (Vptr b ofs) t1 t2 (Vptr b ofs) + | cast_nn_i: forall n t1 t2, + neutral_for_cast t1 -> neutral_for_cast t2 -> + cast (Vint n) t1 t2 (Vint n). (** ** Operational semantics *) -- cgit v1.2.3