From fc36b9c17b8bfd020258944f555d4d9c68eb8dad Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 31 Jan 2021 00:00:37 +0100 Subject: add has_type info --- backend/Selectionproof.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4d075f4a..8f3f5f00 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -783,6 +783,8 @@ Lemma sel_select_opt_correct: Cminor.eval_expr ge sp e m cond vcond -> Cminor.eval_expr ge sp e m a1 v1 -> Cminor.eval_expr ge sp e m a2 v2 -> + Val.has_type v1 ty -> + Val.has_type v2 ty -> Val.bool_of_val vcond b -> env_lessdef e e' -> Mem.extends m m' -> exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'. @@ -792,7 +794,7 @@ Proof. exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC). exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1). exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2). - assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor). + assert (Val.bool_of_val vcond' b) by (inv H5; inv LDC; constructor). exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND). exploit eval_select; eauto. intros (v' & X & Y). exists v'; split; eauto. -- cgit