From 4a3915b34eb9aaa3fd86295ada0548ef2c2a2160 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 14 Jan 2025 15:02:21 +0100
Subject: [PATCH] [Eva] Minor simplification in
[Compute_functions.compute_using_spec].
---
src/plugins/eva/engine/compute_functions.ml | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 5941a06f123..39c0ed11d5c 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 =
--
GitLab