From 952a5faf13280e9bed6fe10670561d7e4fe5bc19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 23:33:53 +0200 Subject: __builtin_expect seems to work --- backend/SplitLong.vp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'backend/SplitLong.vp') 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))). -- cgit