diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 23:33:53 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 23:33:53 +0200 |
| commit | 952a5faf13280e9bed6fe10670561d7e4fe5bc19 (patch) | |
| tree | 7c2bfd73048aa6e7bd991ab25281201d77c70799 /backend/Selectionproof.v | |
| parent | 3b15828ca868365b285ba611ba72177e90d0061b (diff) | |
| download | compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.tar.gz compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.zip | |
__builtin_expect seems to work
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 53600c7a..955c45a4 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -196,12 +196,12 @@ Variable e: env. Variable m: mem. Lemma eval_condexpr_of_expr: - forall a le v b, + forall expected a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr tge sp e m le (condexpr_of_expr a) b. + eval_condexpr tge sp e m le (condexpr_of_expr a expected) b. Proof. - intros until a. functional induction (condexpr_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a expected); intros. (* compare *) inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. |