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/SplitLong.vp | |
| parent | 3b15828ca868365b285ba611ba72177e90d0061b (diff) | |
| download | compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.tar.gz compcert-kvx-952a5faf13280e9bed6fe10670561d7e4fe5bc19.zip | |
__builtin_expect seems to work
Diffstat (limited to 'backend/SplitLong.vp')
| -rw-r--r-- | backend/SplitLong.vp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index dfe42df0..0f240602 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +(* FIXME: expected branching information not propagated *) (** Instruction selection for 64-bit integer operations *) Require String. @@ -256,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) := Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). @@ -278,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) := Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). |