diff options
| author | Kathy Gray | 2016-07-01 14:23:52 +0100 |
|---|---|---|
| committer | Kathy Gray | 2016-07-01 14:24:53 +0100 |
| commit | 25dca699ebdb42e986d98f3a5ae5ff72bc6b6d8d (patch) | |
| tree | 5bfed456bef119478dec0fcabbfd9ad4780e1da8 | |
| parent | 28874bde2f7ad58e76ebe8d779d3920d74ca1db6 (diff) | |
Add missing case to arith_op_no0
Add type refinement to arm spec
| -rw-r--r-- | arm/armv8.sail | 4 | ||||
| -rw-r--r-- | 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 () |