summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-11-10 18:39:51 +0000
committerAlasdair Armstrong2017-11-10 18:39:51 +0000
commitd7ee7d7392d7d4f058cce2e12b7d0336dddb4e17 (patch)
treec953db8e1780a7b80e2f093b72e62047834278c7 /lib
parent05a84d17bf583c97fb3e77c4a6a07d888a6a2681 (diff)
Fixed ocaml backend so it correctly compiles registers passed by name.
Added a test case for this behavior
Diffstat (limited to 'lib')
-rw-r--r--lib/ocaml_rts/sail_lib.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index 176c1124..6876ec35 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -441,6 +441,8 @@ let sqrt_real x = real_of_string (string_of_float (sqrt (Num.float_of_num x)))
let print_int (str, x) =
prerr_endline (str ^ string_of_big_int x)
+let reg_deref r = !r
+
let string_of_zbit = function
| B0 -> "0"
| B1 -> "1"