aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/ValueAOp.v
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-19 21:31:20 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-19 21:31:20 +0100
commit9adb576998f3b2017db5c062b459449e1721579a (patch)
treefd70a6ce92921404c91b7f9f494e219da4ae3945 /mppa_k1c/ValueAOp.v
parentae571e2467e977f03044d750568f6528d8d64e43 (diff)
downloadcompcert-kvx-9adb576998f3b2017db5c062b459449e1721579a.tar.gz
compcert-kvx-9adb576998f3b2017db5c062b459449e1721579a.zip
mul immediate
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