From fa7415be2fe9b240374f0a51c1cd4a9de5376c5a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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 ++++++++++++++++------------
 cfrontend/Cshmgenproof2.v |  6 +++++-
 2 files changed, 21 insertions(+), 13 deletions(-)

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index a76dcb49..5431697f 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 *)
 
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 602e33a9..1a5eaa0a 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -373,7 +373,7 @@ Lemma make_cast_correct:
 Proof.
   unfold make_cast, make_cast1, make_cast2, make_unop.
   intros until v'; intros EVAL CAST.
-  inversion CAST; clear CAST; subst; auto.
+  inversion CAST; clear CAST; subst.
   (* cast_int_int *)
     destruct sz2; destruct si2; repeat econstructor; eauto with cshm.
   (* cast_float_int *)
@@ -382,6 +382,10 @@ Proof.
     destruct sz2; destruct si1; unfold make_floatofint, make_unop; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_float_float *)
     destruct sz2; repeat econstructor; eauto with cshm.
+  (* neutral, ptr *)
+   inversion H0; auto; inversion H; auto.
+  (* neutral, int *)
+   inversion H0; auto; inversion H; auto.
 Qed.
 
 Lemma make_load_correct:
-- 
cgit