summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-03-17 17:39:53 +0000
committerKathy Gray2014-03-17 17:39:53 +0000
commit0e5d48a091c847d773e2305359a7d959f8fac19e (patch)
tree372385e056411db1479c87e386e86cd191bc8fa1 /src
parent42f6ee722ff2b9f49a0b981c0d43aed761098277 (diff)
parent4f1aed40024c8b904e179541c29ef0a2a541752d (diff)
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2
Conflicts: src/test/regbits.sail
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/run_interp.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index a6d74742..37ee7770 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -191,6 +191,11 @@ let rec perform_action ((reg, mem) as env) = function
let old_val = Mem.find (id, n) mem in
let new_val = fupdate_vector_slice old_val value start stop in
V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) new_val mem)
+ (* special case for slices of size 1: wrap value in a vector *)
+ | Write_reg ((Reg (_, _) as r), (Some (start, stop) as slice), value) when eq_big_int start stop ->
+ perform_action env (Write_reg (r, slice, V_vector(zero_big_int, true, [value])))
+ | Write_mem (id, (V_lit(L_aux(L_num _,_)) as n), (Some (start, stop) as slice), value) when eq_big_int start stop ->
+ perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
(* extern functions *)
| Call_extern (name, arg) -> eval_external name arg, env
| _ -> assert false