Permettre les casts entre types de fonction

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 16 insertions, 12 deletions

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 *)