diff options
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 |