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/RTLgenproof.v | |
| parent | 3b15828ca868365b285ba611ba72177e90d0061b (diff) | |
| download | compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.tar.gz compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.zip | |
__builtin_expect seems to work
Diffstat (limited to 'backend/RTLgenproof.v')
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..e62aff22 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -799,11 +799,11 @@ Proof. Qed. Lemma transl_condexpr_CEcond_correct: - forall le cond al vl vb, + forall le cond expected al vl vb, eval_exprlist ge sp e m le al vl -> transl_exprlist_prop le al vl -> eval_condition cond vl m = Some vb -> - transl_condexpr_prop le (CEcond cond al) vb. + transl_condexpr_prop le (CEcond cond expected al) vb. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. |