aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/ValueAOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
-rw-r--r--mppa_k1c/ValueAOp.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 3bb25807..b43c4d78 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -101,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Onegl, v1::nil => negl v1
| Osubl, v1::v2::nil => subl v1 v2
| Omull, v1::v2::nil => mull v1 v2
+ | Omullimm n, v1::nil => mull v1 (L n)
| Omullhs, v1::v2::nil => mullhs v1 v2
| Omullhu, v1::v2::nil => mullhu v1 v2
| Odivl, v1::v2::nil => divls v1 v2