diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml index dae5dc6c27e651ab6cffeafd718d4619878bb54d..edd21f3ac73dcfef5a4db49fae648c980ad05c38 100644 --- a/src/plugins/e-acsl/src/code_generator/injector.ml +++ b/src/plugins/e-acsl/src/code_generator/injector.ml @@ -49,20 +49,22 @@ let replace_literal_strings_in_args env kf_opt (* None for globals *) args = RTL. *) let rename_caller ~loc caller args = 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 the RTL. *) let fvi = Rtl.Symbols.libc_replacement caller in fvi, args end 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 from the above because argument list of format functions is extended with an argument describing actual variadic arguments *) (* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *) 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 else caller, args diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml index 1d3a07fb89529b5d1072e90ab653243fc3333da6..ab11845a3d08fddbbc59ed0afe1c348e7c5c9c2c 100644 --- a/src/plugins/e-acsl/src/project_initializer/rtl.ml +++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml @@ -79,7 +79,7 @@ end = struct with Not_found -> raise (Unregistered s) 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 find_vi name with Unregistered _ ->