summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--riscv/platform_impl.ml2
-rw-r--r--riscv/platform_main.ml30
2 files changed, 14 insertions, 18 deletions
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index 342eab35..a1a1f699 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -27,7 +27,7 @@ let uint64_to_bytes u = let open Int64 in
let reset_vec_size = 8l;;
let reset_vec_int start_pc = [
- 0x267l; (* auipc t0, 0x0 *)
+ 0x297l; (* auipc t0, 0x0 *)
(let open Int32 in
add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi a1, t0, ofs(dtb) *)
0xf1402573l; (* csrr a0, mhartid *)
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index 73497aa5..b4a468f9 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -50,7 +50,7 @@
open Elf_loader
open Sail_lib
-open Riscv;;
+open Riscv
(* OCaml driver for generated RISC-V model. *)
@@ -61,8 +61,7 @@ let options = Arg.align []
let usage_msg = "RISC-V platform options:"
let elf_arg =
- Arg.parse options (fun s ->
- opt_file_arguments := !opt_file_arguments @ [s])
+ Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s])
usage_msg;
( match !opt_file_arguments with
| f :: _ -> print_endline ("Loading ELF file " ^ f); f
@@ -72,20 +71,17 @@ let elf_arg =
let () =
Random.self_init ();
- zPC := Platform.init elf_arg;
+ let pc = Platform.init elf_arg in
sail_call
(fun r ->
- begin
- zPC := (z__GetSlice_int ((Big_int.of_string "64"), (Elf_loader.elf_entry ()), (Big_int.of_string "0")));
- begin
- try ( zinit_sys ();
- zloop (Elf_loader.elf_tohost ())
- )
- with
- | ZError_not_implemented (zs) ->
- print_string ("Error: Not implemented: ", zs)
- | ZError_internal_error (_) ->
- prerr_endline "Error: internal error"
- end
- end)
+ try ( zinit_sys ();
+ zPC := pc;
+ zloop (Elf_loader.elf_tohost ())
+ )
+ with
+ | ZError_not_implemented (zs) ->
+ print_string ("Error: Not implemented: ", zs)
+ | ZError_internal_error (_) ->
+ prerr_endline "Error: internal error"
+ )