From 0d2f4a416abcc44fb000758a134a38562a5d6d19 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 17 Oct 2007 08:55:50 +0000
Subject: [PATCH] Relaxation de la regle d'evaluation Ecast
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@420 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
cfrontend/Csem.v | 4 ++--
cfrontend/Cshmgenproof3.v | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index af601acae..8d8f88a30 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -562,10 +562,10 @@ Inductive eval_expr: expr -> val -> Prop :=
eval_expr a2 v2 ->
bool_of_val v2 (typeof a2) v ->
eval_expr (Expr (Eandbool a1 a2) ty) v
- | eval_Ecast: forall a ty v1 v,
+ | eval_Ecast: forall a ty ty' v1 v,
eval_expr a v1 ->
cast v1 (typeof a) ty v ->
- eval_expr (Expr (Ecast ty a) ty) v
+ eval_expr (Expr (Ecast ty a) ty') v
(** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
in l-value position. The result is the memory location [b, ofs]
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 54f9b7727..2b2cefbc7 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -628,10 +628,10 @@ Proof.
Qed.
Lemma transl_Ecast_correct:
- forall (a : Csyntax.expr) (ty : type) (v1 v : val),
+ forall (a : Csyntax.expr) (ty ty': type) (v1 v : val),
Csem.eval_expr ge e m a v1 ->
eval_expr_prop a v1 ->
- cast v1 (typeof a) ty v -> eval_expr_prop (Expr (Ecast ty a) ty) v.
+ cast v1 (typeof a) ty v -> eval_expr_prop (Expr (Ecast ty a) ty') v.
Proof.
intros; red; intros. inversion WT; clear WT; subst. monadInv TR.
eapply make_cast_correct; eauto.
--
GitLab