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/ValueAOp.v | |
| parent | 2227019e15866870f87488630f17cbb0797d1786 (diff) | |
| download | compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.tar.gz compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.zip | |
long nand, nor, nxor
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 15378811..33f4d8a9 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -101,10 +101,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omodlu, v1::v2::nil => modlu v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlimm n, v1::nil => andl v1 (L n) + | Onandl, v1::v2::nil => notl (andl v1 v2) + | Onandlimm n, v1::nil => notl (andl v1 (L n)) | Oorl, v1::v2::nil => orl v1 v2 | Oorlimm n, v1::nil => orl v1 (L n) + | Onorl, v1::v2::nil => notl (orl v1 v2) + | Onorlimm n, v1::nil => notl (orl v1 (L n)) | Oxorl, v1::v2::nil => xorl v1 v2 | Oxorlimm n, v1::nil => xorl v1 (L n) + | Onxorl, v1::v2::nil => notl (xorl v1 v2) + | Onxorlimm n, v1::nil => notl (xorl v1 (L n)) | Oshll, v1::v2::nil => shll v1 v2 | Oshllimm n, v1::nil => shll v1 (I n) | Oshrl, v1::v2::nil => shrl v1 v2 |