From 25dca699ebdb42e986d98f3a5ae5ff72bc6b6d8d Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 1 Jul 2016 14:23:52 +0100
Subject: Add missing case to arith_op_no0 Add type refinement to arm spec

---
 arm/armv8.sail                | 4 ++--
 src/lem_interp/interp_lib.lem | 4 +++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/arm/armv8.sail b/arm/armv8.sail
index a398e52d..e7e27c17 100644
--- a/arm/armv8.sail
+++ b/arm/armv8.sail
@@ -877,7 +877,7 @@ function clause execute ( LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,me
   (bit[64]) address := 0; (* ARM: uninitialized *)
   (bit['D]) data1 := 0; (* ARM: uninitialized *)
   (bit['D]) data2 := 0; (* ARM: uninitialized *)
-  (*constant*) (uinteger) dbytes := datasize quot 8;
+  (*constant*) ([|1:8|]) dbytes := datasize quot 8;
   (boolean) rt_unknown := false;
 
   if memop == MemOp_LOAD & t == t2 then {
@@ -1359,7 +1359,7 @@ function clause execute ( LoadStorePair(wback,postindex,n,t,t2,acctype,memop,_si
   (bit[64]) address := 0; (* ARM: uninitialized *)
   (bit['D]) data1 := 0; (* ARM: uninitialized *)
   (bit['D]) data2 := 0; (* ARM: uninitialized *)
-  (*constant*) (uinteger) dbytes := datasize quot 8;
+  (*constant*) ([|1:8|]) dbytes := datasize quot 8;
   (boolean) rt_unknown := false;
   (boolean) wb_unknown := false;
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 2922db67..5783a095 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -573,7 +573,9 @@ let arith_op_no0 op v =
       | (V_lit(L_aux (L_num x) lx), V_lit(L_aux (L_num y) ly)) -> 
 	if y = 0 
 	then V_lit (L_aux L_undef ly)
-	else V_lit(L_aux (L_num (op x y)) lx)
+        else V_lit(L_aux (L_num (op x y)) lx)
+      | (V_lit (L_aux L_undef lx),_) -> vl
+      | (_, (V_lit (L_aux L_undef ly))) -> vr
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
       | _ -> fail ()
-- 
cgit v1.2.3