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 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm') 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; -- cgit v1.2.3