From 8e39b37aa849bcd50cb45f3084b97befe12d086f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 14 Jan 2025 11:01:16 +0100
Subject: [PATCH] [Eva] use proper printer for variable names
---
src/plugins/eva/engine/compute_functions.ml | 3 ++-
src/plugins/eva/utils/library_functions.ml | 4 ++--
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 39c0ed11d5c..84a84a278f1 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -238,7 +238,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let vi = Kernel_function.get_vi call.kf in
(* Use vorig_name to avoid message duplication due to variadic renaming. *)
Self.feedback ~once:true
- "@[using specification for function %s@]" vi.vorig_name;
+ "@[using specification for function %a@]"
+ Printer.pp_varname vi.vorig_name;
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
let states =
diff --git a/src/plugins/eva/utils/library_functions.ml b/src/plugins/eva/utils/library_functions.ml
index 60010cc0b70..7346568c1d6 100644
--- a/src/plugins/eva/utils/library_functions.ml
+++ b/src/plugins/eva/utils/library_functions.ml
@@ -109,9 +109,9 @@ let warn_unsupported_spec name =
let header = Hashtbl.find unsupported_specs_tbl name in
Self.warning ~once:true ~current:true
~wkey:Self.wkey_libc_unsupported_spec
- "@[The specification of function '%s' is currently not supported by Eva.@ \
+ "@[The specification of function '%a' is currently not supported by Eva.@ \
Consider adding '%a'@ to the analyzed source files.@]"
- name Filepath.Normalized.pretty
+ Printer.pp_varname name Filepath.Normalized.pretty
(Filepath.Normalized.concat System_config.Share.libc header)
with Not_found -> ()
--
GitLab