diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 21:48:12 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 21:48:12 +0200 |
| commit | a1c645892fda697675605f446f86fef90d43971d (patch) | |
| tree | a7a0f57977bc545eabad1eb13e11de9cea91f252 /mppa_k1c/SelectOp.vp | |
| parent | e08d244a18870131820814880685504f0ea467e6 (diff) | |
| download | compcert-kvx-a1c645892fda697675605f446f86fef90d43971d.tar.gz compcert-kvx-a1c645892fda697675605f446f86fef90d43971d.zip | |
ternary ops work on (unsigned/signed) int with test on signed int
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 6 |
1 files changed, 3 insertions, 3 deletions
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. |