From 63fccf3902edbeb7816e6c419b0cbdcfea423cb9 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 10 Jul 2018 22:39:23 +0100
Subject: Update CHERI code extraction from Isabelle

Also use zero-initialised memory.  Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.
---
 mips/mips_extras.lem | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'mips')

diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 86e78586..4edb0066 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -111,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
-- 
cgit v1.2.3