diff options
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 14753871..4b64e495 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -275,7 +275,12 @@ Nondetfunction xor (e1: expr) (e2: expr) := (** ** Integer logical negation *) -Definition notint (e: expr) := xorimm Int.mone e. +Nondetfunction notint (e: expr) := + match e with + | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil) + | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil) + | _ => xorimm Int.mone e + end. (** ** Integer division and modulus *) |