Skip to content
Snippets Groups Projects
Commit 0d00f5d4 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Use the `vorig_name` of a function when checking for replacements

parent f5cfd9b3
No related branches found
No related tags found
No related merge requests found
...@@ -49,20 +49,22 @@ let replace_literal_strings_in_args env kf_opt (* None for globals *) args = ...@@ -49,20 +49,22 @@ let replace_literal_strings_in_args env kf_opt (* None for globals *) args =
RTL. *) RTL. *)
let rename_caller ~loc caller args = let rename_caller ~loc caller args =
if Options.Replace_libc_functions.get () if Options.Replace_libc_functions.get ()
&& Functions.RTL.has_rtl_replacement caller.vname then begin && Functions.RTL.has_rtl_replacement caller.vorig_name then begin
(* rewrite names of functions for which we have alternative definitions in (* rewrite names of functions for which we have alternative definitions in
the RTL. *) the RTL. *)
let fvi = Rtl.Symbols.libc_replacement caller in let fvi = Rtl.Symbols.libc_replacement caller in
fvi, args fvi, args
end end
else if Options.Validate_format_strings.get () else if Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name caller.vname then && Functions.Libc.is_printf_name caller.vorig_name then
(* rewrite names of format functions (such as printf). This case differs (* rewrite names of format functions (such as printf). This case differs
from the above because argument list of format functions is extended with from the above because argument list of format functions is extended with
an argument describing actual variadic arguments *) an argument describing actual variadic arguments *)
(* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *) (* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
let fvi = Rtl.Symbols.libc_replacement caller in let fvi = Rtl.Symbols.libc_replacement caller in
let fmt = Functions.Libc.get_printf_argument_str ~loc caller.vname args in let fmt =
Functions.Libc.get_printf_argument_str ~loc caller.vorig_name args
in
fvi, fmt :: args fvi, fmt :: args
else else
caller, args caller, args
......
...@@ -79,7 +79,7 @@ end = struct ...@@ -79,7 +79,7 @@ end = struct
with Not_found -> raise (Unregistered s) with Not_found -> raise (Unregistered s)
let libc_replacement fvi = let libc_replacement fvi =
let name = Functions.RTL.libc_replacement_name fvi.vname in let name = Functions.RTL.libc_replacement_name fvi.vorig_name in
try try
find_vi name find_vi name
with Unregistered _ -> with Unregistered _ ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment