From 3babc5a0c35a2774904d2ee44f3c69e79c54876f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 15 May 2018 17:02:23 +0100
Subject: Some tweaks to ocaml compilation and sail_lib for ARM with system
 registers

---
 src/ocaml_backend.ml |  4 ++--
 src/sail_lib.ml      | 14 +++++++++++++-
 2 files changed, 15 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 60a34273..a13d7b4b 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -177,9 +177,9 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
   | P_id id ->
      begin
        match Env.lookup_id id (pat_env_of pat) with
-       | Local (Immutable, _) | Unbound -> zencode ctx id
+       | Local (_, _) | Unbound -> zencode ctx id
        | Enum _ -> zencode_upper ctx id
-       | _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat)
+       | _ -> failwith ("Ocaml: Cannot pattern match on register: " ^ string_of_pat pat)
      end
   | P_lit lit -> ocaml_lit lit
   | P_typ (_, pat) -> ocaml_pat ctx pat
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 08de6d69..28784ce1 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -49,7 +49,7 @@ let trace_call str =
 type bit = B0 | B1
 
 let eq_bit (a, b) = a = b
-                  
+
 let and_bit = function
   | B1, B1 -> B1
   | _, _ -> B0
@@ -629,3 +629,15 @@ let speculate_conditional_success () = true
 (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *)
 let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ()))
 
+let string_of_bool = function
+  | true -> "true"
+  | false -> "false"
+
+let dec_str x = Big_int.to_string x
+
+let hex_str x = Big_int.to_string x
+
+let trace_memory_write (_, _, _) = ()
+let trace_memory_read (_, _, _) = ()
+
+let sleep_request () = ()
-- 
cgit v1.2.3