diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 19:47:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 19:47:03 +0100 |
| commit | 7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d (patch) | |
| tree | 626ffb1662cdb76fcf2979291c7adda9bacbe63f /mppa_k1c/SelectLong.vp | |
| parent | 2227019e15866870f87488630f17cbb0797d1786 (diff) | |
| download | compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.tar.gz compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.zip | |
long nand, nor, nxor
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 5e94fbb5..cc266abd 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -287,8 +287,17 @@ Nondetfunction xorl (e1: expr) (e2: expr) := (** ** Integer logical negation *) -Definition notl (e: expr) := - if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. +Nondetfunction notl (e: expr) := + match e with + | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil) + | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil) + | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil) + | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil) + | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil) + | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil) + | _ => xorlimm Int64.mone e + end. +(* old: if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *) (** ** Integer division and modulus *) |