From a1c645892fda697675605f446f86fef90d43971d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 21:48:12 +0200 Subject: ternary ops work on (unsigned/signed) int with test on signed int --- mppa_k1c/SelectOp.vp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/SelectOp.vp') diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 10c91bba..906d6791 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -63,7 +63,7 @@ Context {hf: helper_functions}. (** Ternary operator *) Definition select o0 o1 oselect := - Eop (Oselect (Ccomp0 Ceq)) + Eop (Oselect (Ccomp0 Cne)) (o0:::o1:::oselect:::Enil). (** ** Constants **) @@ -288,7 +288,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then Eop (Oselect (Ccomp0 Cne)) (v0:::v1:::y0:::Enil) + then select v0 v1 y0 else Eop Oor (e1:::e2:::Enil) | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) (y0:::Enil)):::Enil)):::v0:::Enil)), @@ -297,7 +297,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then Eop (Oselect (Ccompu0 Cne)) (v0:::v1:::y0:::Enil) + then select v0 v1 y0 else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. -- cgit