diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 3 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf_cheri128.ml | 2 |
4 files changed, 4 insertions, 5 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index aad7418d..63dd0d76 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -466,8 +466,7 @@ let translate_address top_level end_flag thunk_name registers address = (fun _ -> Interp.resume int_mode (Interp.Thunk_frame - (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) - [arg;E_aux (E_lit (L_aux (L_num 0) Interp_ast.Unknown)) (Interp_ast.Unknown,Nothing)]) + (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in match (address_error) with diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 3538dd44..6ce5d5e8 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1296,7 +1296,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index a0f2a951..546fe6c8 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1388,7 +1388,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 01e9bd2d..4c881b04 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1388,7 +1388,7 @@ let run () = (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) - let addr_trans = translate_address context E_little_endian "TranslateAddress" in + let addr_trans = translate_address context E_little_endian "TranslatePC" in if String.length(!raw_file) != 0 then load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; |