From 6e64e970a706c45b5b236a0e4f92698e22682344 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 07:56:33 +0200 Subject: adapt the other targets for the new field in CEcond --- powerpc/SelectOp.vp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 50b1bdd6..52f4f855 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -472,7 +472,7 @@ Definition intuoffloat (e: expr) := else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. -- cgit