diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-31 00:00:37 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-31 00:00:37 +0100 |
| commit | fc36b9c17b8bfd020258944f555d4d9c68eb8dad (patch) | |
| tree | ec485e5c1464e84b9c94da4b876538f9810196a3 | |
| parent | 9324c5f828db278d48a0bef9e6cc685da41c2a4b (diff) | |
| download | compcert-kvx-fc36b9c17b8bfd020258944f555d4d9c68eb8dad.tar.gz compcert-kvx-fc36b9c17b8bfd020258944f555d4d9c68eb8dad.zip | |
add has_type info
| -rw-r--r-- | backend/Selectionproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
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. |