From 0d00f5d47dab03f4f48560bcedb055a8f31d0633 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 22 Jun 2021 18:20:19 +0200
Subject: [PATCH] [eacsl] Use the `vorig_name` of a function when checking for
replacements
---
src/plugins/e-acsl/src/code_generator/injector.ml | 8 +++++---
src/plugins/e-acsl/src/project_initializer/rtl.ml | 2 +-
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index dae5dc6c27e..edd21f3ac73 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 1d3a07fb895..ab11845a3d0 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 _ ->
--
GitLab