diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index 39c0ed11d5ce017137872089b4a9d9130d640188..84a84a278f1bf8f92bd33cd65d43249b3dad5bbb 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 60010cc0b707b7d699061f7dfd524677f9ed8432..7346568c1d647fad0bdbea66a2d70aaeaa5b0abe 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 -> ()