diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml index 5941a06f12309e60642b16a3a34e8b209dce100e..39c0ed11d5ce017137872089b4a9d9130d640188 100644 --- a/src/plugins/eva/engine/compute_functions.ml +++ b/src/plugins/eva/engine/compute_functions.ml @@ -235,11 +235,10 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct let compute_using_spec spec kinstr call state = if Parameters.InterpreterMode.get () then Self.abort "Library function call. Stopping."; - (* Use vorig_name in message to avoid variadic renaming *) - let kf_orig_name = (Kernel_function.get_vi call.kf).vorig_name in - Self.feedback ~once:true - "@[using specification for function %s@]" kf_orig_name; 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; if Cil.is_in_libc vi.vattr then Library_functions.warn_unsupported_spec vi.vorig_name; let states =