summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/run_with_elf.ml12
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml16
-rw-r--r--src/lem_interp/run_with_elf_cheri128.ml16
3 files changed, 22 insertions, 22 deletions
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 8533827b..0dadc007 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name =
aarch64_register_data_all) *)
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -736,11 +736,11 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Mips.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 46bc92fb..2bf84e2d 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
match Nat_big_num.to_int e_machine with
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Cheri.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.read_memory_tagged_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.memory_vals_tagged,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_read_memory_tagged_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_memory_vals_tagged,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 5e5bee21..e4d91c41 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
match Nat_big_num.to_int e_machine with
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
(Cheri128.defs,
- (Mips_extras.read_memory_functions,
- Mips_extras.read_memory_tagged_functions,
- Mips_extras.memory_writes,
- Mips_extras.memory_eas,
- Mips_extras.memory_vals,
- Mips_extras.memory_vals_tagged,
- Mips_extras.barrier_functions),
+ (Mips_extras.mips_read_memory_functions,
+ Mips_extras.mips_read_memory_tagged_functions,
+ Mips_extras.mips_memory_writes,
+ Mips_extras.mips_memory_eas,
+ Mips_extras.mips_memory_vals,
+ Mips_extras.mips_memory_vals_tagged,
+ Mips_extras.mips_barrier_functions),
[],
MIPS,
D_decreasing,