From 9adb576998f3b2017db5c062b459449e1721579a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 21:31:20 +0100
Subject: mul immediate

---
 mppa_k1c/SelectOp.vp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mppa_k1c/SelectOp.vp')

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 22211167..d87c837e 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -173,7 +173,7 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: j :: nil =>
       Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
   | _ =>
-      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
+      Eop (Omulimm n1) (e2 ::: Enil)
   end.
 
 Nondetfunction mulimm (n1: int) (e2: expr) :=
-- 
cgit