diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 20 | ||||
| -rw-r--r-- | src/lem_interp/run_with_elf.ml | 5 |
2 files changed, 15 insertions, 10 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index d1e1672e..d65814f3 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -336,24 +336,28 @@ let translate_address top_level end_flag thunk_name address = (fun _ -> Interp.resume int_mode (Interp.Thunk_frame - (E_aux (E_app (Id_aux (Id thunk_name) Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) + (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)]) + (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "translate top level") Interp.Top) Nothing) in match (address,error) with | (Just addr, _) -> (match addr with - | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ v; - Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _))] -> + | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _)); + Interp.V_ctor (Id_aux (Id "Some") _) _ _ v] -> let (mem_v,_) = extern_mem_value mode v in ((address_of_memory_value end_flag mem_v), Just n) - | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ v; - Interp.V_ctor (Id_aux (Id "None") _) _ _ _] -> + | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "None") _) _ _ _; + Interp.V_ctor (Id_aux (Id "Some") _) _ _ v] -> let (mem_v,_) = extern_mem_value mode v in ((address_of_memory_value end_flag mem_v), Nothing) - | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "None") _) _ _ _; - Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _))] -> + | Interp.V_tuple[Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_num n) _)); + Interp.V_ctor (Id_aux (Id "None") _) _ _ _] -> (Nothing, Just n) | _ -> (Nothing,Nothing) end) - | (Nothing, Just err) -> (Nothing,Nothing) + | (Nothing, Just err) -> match err with + | Internal_error msg -> Assert_extra.failwith msg + | _ -> Assert_extra.failwith "Not an internal error either" end end diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 6324f193..deafd92a 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -972,10 +972,11 @@ 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_big_endian "translate_address" in + let addr_trans = translate_address context E_big_endian "TranslateAddress" in let startaddr,startaddr_internal = match addr_trans startaddr_internal with | Some a, _ -> integer_of_address a, a - | None, _ -> failwith "Address translation failed in some way" + | None, Some i -> failwith ("Address translation failed with error code " ^ (Nat_big_num.to_string i)) + | _ -> failwith "Neither an address or a code on translate address" in let initial_opcode = Opcode (List.map (fun b -> match b with | Some b -> b |