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: [PATCH] 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 a76dcb492..5431697fa 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 602e33a97..1a5eaa0ac 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:
--
GitLab