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/RTLgen.v | |
| parent | 3b15828ca868365b285ba611ba72177e90d0061b (diff) | |
| download | compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.tar.gz compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.zip | |
__builtin_expect seems to work
Diffstat (limited to 'backend/RTLgen.v')
| -rw-r--r-- | backend/RTLgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ac98f3a1..243d7b7c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -477,9 +477,9 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) {struct a} : mon node := match a with - | CEcond c al => + | CEcond c expected al => do rl <- alloc_regs map al; - do nt <- add_instr (Icond c rl ntrue nfalse None); + do nt <- add_instr (Icond c rl ntrue nfalse expected); transl_exprlist map al rl nt | CEcondition a b c => do nc <- transl_condexpr map c ntrue nfalse; |