diff options
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index b43c4d78..fb1977ea 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -132,6 +132,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrlu, v1::v2::nil => shrlu v1 v2 | Oshrluimm n, v1::nil => shrlu v1 (I n) | Oshrxlimm n, v1::nil => shrxl v1 (I n) + | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) + | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 |