summaryrefslogtreecommitdiff
path: root/mips/mips_extras.lem
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-07-24 18:09:18 +0100
committerAlasdair Armstrong2018-07-24 18:09:18 +0100
commit6b4f407ad34ca7d4d8a89a5a4d401ac80c7413b0 (patch)
treeed09b22b7ea4ca20fbcc89b761f1955caea85041 /mips/mips_extras.lem
parentdafb09e7c26840dce3d522fef3cf359729ca5b61 (diff)
parent8114501b7b956ee4a98fa8599c7efee62fc19206 (diff)
Merge remote-tracking branch 'origin/sail2' into c_fixes
Diffstat (limited to 'mips/mips_extras.lem')
-rw-r--r--mips/mips_extras.lem8
1 files changed, 6 insertions, 2 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 2e07586c..4edb0066 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -90,7 +90,6 @@ let shift_bits_right_arith v n =
maybe_fail "shift_bits_right_arith" r
(* Use constants for undefined values for now *)
-let internal_pick vs = return (head vs)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)
@@ -112,7 +111,12 @@ val elf_entry : unit -> integer
let elf_entry () = 0
declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
-let print_bits msg bs = prerr_endline (msg ^ (string_of_bv bs))
+let print_bits msg bs = print_endline (msg ^ (string_of_bv bs))
+let prerr_bits msg bs = prerr_endline (msg ^ (string_of_bv bs))
+
+val prerr_string : string -> unit
+let prerr_string _ = ()
+declare ocaml target_rep function prerr_string = `Pervasives.prerr_string`
val get_time_ns : unit -> integer
let get_time_ns () = 0