3 files changed, 7 insertions, 20 deletions
diff --git a/test/isabelle/elf_loader.ml b/test/isabelle/elf_loader.ml
index f68e6693..6ec89ee6 100644
--- a/test/isabelle/elf_loader.ml
+++ b/test/isabelle/elf_loader.ml
@@ -65,9 +65,9 @@ let rec break n = function
   | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs)
 
 let print_segment seg =
-  let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in
+  let bs = seg.Elf_interpreted_segment.elf64_segment_body in
   prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
-  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs)
+  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
 
 let read name =
   let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
@@ -110,19 +110,6 @@ let write_file chan paddr i byte =
   output_string chan (Nat_big_num.to_string (Nat_big_num.add paddr (Nat_big_num.of_int i)) ^ "\n");
   output_string chan (string_of_int byte ^ "\n")
 
-(*let load_segment ?writer:(writer=write_sail_lib) seg =
-  let open Elf_interpreted_segment in
-  let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
-  let paddr = seg.elf64_segment_paddr in
-  let base = seg.elf64_segment_base in
-  let offset = seg.elf64_segment_offset in
-  prerr_endline "\nLoading Segment";
-  prerr_endline ("Segment offset: " ^ Nat_big_num.to_string offset);
-  prerr_endline ("Segment base address: " ^ Nat_big_num.to_string base);
-  prerr_endline ("Segment physical address: " ^ Nat_big_num.to_string paddr);
-  print_segment seg;
-  List.iteri (writer paddr) (List.map int_of_char bs)*)
-
 let load_elf name =
   let segments, e_entry, symbol_map = read name in
   opt_elf_entry := e_entry;
diff --git a/test/isabelle/run_aarch64.ml b/test/isabelle/run_aarch64.ml
index 67600e81..c6037866 100644
--- a/test/isabelle/run_aarch64.ml
+++ b/test/isabelle/run_aarch64.ml
@@ -69,7 +69,7 @@ let liftS = Aarch64.liftState (Aarch64.get_regval, Aarch64.set_regval)
 let load_elf_segment seg =
   let open Elf_interpreted_segment in
   let open Aarch64_export in
-  let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
+  let bs = seg.elf64_segment_body in
   let paddr = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_paddr) in
   let base = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_base) in
   let offset = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_offset) in
@@ -79,7 +79,7 @@ let load_elf_segment seg =
   prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base);
   prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr);
   print_segment seg;
-  Aarch64.iteriS writer bs
+  Aarch64.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs)
 
 let _ =
   Random.self_init ();
diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml
index 1f9fbc0e..e6d752b7 100644
--- a/test/isabelle/run_cheri.ml
+++ b/test/isabelle/run_cheri.ml
@@ -68,7 +68,7 @@ let liftS = State.liftState (Cheri_types.get_regval, Cheri_types.set_regval)
 
 let load_elf_segment seg =
   let open Elf_interpreted_segment in
-  let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
+  let bs = seg.elf64_segment_body in
   let paddr = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_paddr) in
   let base = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_base) in
   let offset = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_offset) in
@@ -78,7 +78,7 @@ let load_elf_segment seg =
   prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base);
   prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr);
   print_segment seg;
-  State.iteriS writer bs
+  State.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs)
 
 let _ =
   Random.self_init ();
@@ -86,7 +86,7 @@ let _ =
     | f :: _ -> load_elf f
     | _ -> []
   in
-  State_monad.prerr_results
+  (* State_monad.prerr_results *)
     (Cheri_code.initial_state |>
     (State.iterS load_elf_segment elf_segments >> (fun _ ->
     liftS (Cheri.main ()))));