summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-07-13 10:15:30 +0100
committerBrian Campbell2018-07-13 10:15:30 +0100
commit82784b669df18e33c48449020f29f36980d12bf3 (patch)
treee8c9d854b3edd3d34c64e745705e9cce4dc877a1 /src/value.ml
parent6586abcc185fa4e0f3853a73d91f097fbde16aca (diff)
parent3c4a27d7041d71fb229970dacab013cf84669755 (diff)
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml4
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