diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/run_interp.ml | 5 | ||||
| -rw-r--r-- | src/test/regbits.sail | 2 |
2 files changed, 6 insertions, 1 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 diff --git a/src/test/regbits.sail b/src/test/regbits.sail index 5bc799bb..a49f0f97 100644 --- a/src/test/regbits.sail +++ b/src/test/regbits.sail @@ -13,7 +13,7 @@ function (bit[64]) main _ = { f := XER; (bit[7]) foo := XER[57..63]; query := XER.SO; - XER.SO := bitone; + XER.SO := 0b1; XER.FOOBAR := 0b11; XER } |