diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 11:26:50 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 11:26:50 +0200 |
| commit | 4b78052471c339c1e7dbbabe9ac20835fe963b9c (patch) | |
| tree | 2c38cb8c477175f1cc0f1eb4e8a4585b3188e30b /mppa_k1c/SelectOp.vp | |
| parent | 7e921e5ac243b453e6ec856abd5af2eed810226d (diff) | |
| download | compcert-kvx-4b78052471c339c1e7dbbabe9ac20835fe963b9c.tar.gz compcert-kvx-4b78052471c339c1e7dbbabe9ac20835fe963b9c.zip | |
some more simplifications
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index c5a86ac1..72f5616c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -327,7 +327,12 @@ Nondetfunction or (e1: expr) (e2: expr) := end. Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else + if Int.eq n1 Int.zero + then e2 + else + if Int.eq n1 Int.mone + then Eop Onot (e2:::Enil) + else match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil | Eop (Oxorimm n2) (t2:::Enil) => |