diff options
| author | Robert Norton | 2018-07-12 15:54:11 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-07-12 15:54:15 +0100 |
| commit | 79ecf8b83b06a6bd1330e1f243826cbe951a9e7d (patch) | |
| tree | 5d3b76bdc57d48af47a37bc5580f2d88d1997c2a /src/value.ml | |
| parent | 8195ac7e4d851e9901bfaae92997ea51914c09b2 (diff) | |
update arm and mips models for new type of write_ram builtin. Also fix c and interpreter implementations of same.
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/value.ml b/src/value.ml index 1d2346af..dccb216e 100644 --- a/src/value.ml +++ b/src/value.ml @@ -406,8 +406,8 @@ let value_read_ram = function let value_write_ram = function | [v1; v2; v3; v4; v5] -> - Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5); - V_unit + let b = Sail_lib.write_ram (coerce_int v1, coerce_int v2, coerce_bv v3, coerce_bv v4, coerce_bv v5) in + V_bool(b) | _ -> failwith "value write_ram" let value_load_raw = function |
