diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index fd44697b05b549db2a2b78bb62a481e54fc85819..5941a06f12309e60642b16a3a34e8b209dce100e 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -235,8 +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 %a@]" Kernel_function.pretty call.kf;
+ "@[using specification for function %s@]" kf_orig_name;
let vi = Kernel_function.get_vi call.kf in
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
diff --git a/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle b/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle
index 0c1758790c3f740c0277e62e36faf1c90bc09a1d..ea61b8a1a4d92c80cbafeb5d8e2d384304811fe3 100644
--- a/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/redefine_anonymous_parameters.res.oracle
@@ -7,7 +7,7 @@
[variadic] redefine_anonymous_parameters.i:4:
Translating call to printf to a call to the specialized version printf_va_1.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 03338e671a19f53d2f30031af1fd07be981405d3..1da3a3b77a3c13cd853560b8888d5e9d7842e666 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -42,7 +42,7 @@
[kernel:annot:missing-spec] exec.c:15: Warning:
Neither code nor specification for function execlp_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function execlp_fallback_1
+[eva] using specification for function execlp
[eva:invalid-assigns] exec.c:15:
Completely invalid destination for assigns clause *(param1 + (0 ..)).
Ignoring.
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index b15b13096bcb1e49c35dbeff48745f6d97a0f9ca..9448251dd8ba0be85ff72fcfde67e101411ceb66 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -40,7 +40,7 @@
[kernel:annot:missing-spec] fcntl.c:16: Warning:
Neither code nor specification for function fcntl_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function fcntl_fallback_1
+[eva] using specification for function fcntl
[eva:alarm] fcntl.c:20: Warning:
function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
[eva:alarm] fcntl.c:24: Warning:
@@ -48,7 +48,6 @@
[kernel:annot:missing-spec] fcntl.c:28: Warning:
Neither code nor specification for function fcntl_fallback_2,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function fcntl_fallback_2
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
fl ∈ [--..--] or UNINITIALIZED
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index ec407450fca075e637fbac4844156acce805af8d..89c49a920e72ce1dbf2d73951ed407554a4e8a16 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -24,7 +24,7 @@
[kernel:annot:missing-spec] open.c:9: Warning:
Neither code nor specification for function open_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function open_fallback_1
+[eva] using specification for function open
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
flag ∈ {0}
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index ae94f9c59c8d45aaec0c8e915db1fc6ea956ba44..338a8d81adae5d6022448a3e6cccec5ce8712eed 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -16,7 +16,7 @@
[kernel:annot:missing-spec] open_wrong.c:13: Warning:
Neither code nor specification for function open_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function open_fallback_1
+[eva] using specification for function open
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
file ∈ {{ "file" }}
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index e45e5dc8e0738d07fb9f66dbbfa7e08f2ccd5584..89a7c6689009511192f5e3a04d8cdfb04ed2cda7 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -23,7 +23,7 @@
[kernel:annot:missing-spec] openat.c:10: Warning:
Neither code nor specification for function openat_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function openat_fallback_1
+[eva] using specification for function openat
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
flag ∈ {0}
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index a567cee9c488f9d959f6468f74e8a83f50f11284..a4bc497d2519e7a7a1689ca4ddb35ae17826dbcc 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -97,49 +97,17 @@
[variadic] printf.c:80:
Translating call to printf to a call to the specialized version printf_va_32.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
-[eva] using specification for function printf_va_2
-[eva] using specification for function printf_va_3
-[eva] using specification for function printf_va_4
-[eva] using specification for function printf_va_5
-[eva] using specification for function printf_va_6
-[eva] using specification for function printf_va_7
-[eva] using specification for function printf_va_8
-[eva] using specification for function printf_va_9
-[eva] using specification for function printf_va_10
-[eva] using specification for function printf_va_11
-[eva] using specification for function printf_va_12
-[eva] using specification for function printf_va_13
-[eva] using specification for function printf_va_14
-[eva] using specification for function printf_va_15
-[eva] using specification for function printf_va_16
-[eva] using specification for function printf_va_17
-[eva] using specification for function printf_va_18
-[eva] using specification for function printf_va_19
-[eva] using specification for function printf_va_20
-[eva] using specification for function printf_va_21
-[eva] using specification for function printf_va_22
-[eva] using specification for function printf_va_23
-[eva] using specification for function printf_va_24
-[eva] using specification for function printf_va_25
+[eva] using specification for function printf
[eva:garbled-mix:assigns] printf.c:68:
The specification of function printf_va_25
has generated a garbled mix of addresses
for assigns clause __fc_stdout->__fc_FILE_data.
-[eva] using specification for function printf_va_26
[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function printf_fallback_1
[eva:invalid-assigns] printf.c:71:
Completely invalid destination for assigns clause *(param1 + (0 ..)).
Ignoring.
-[eva] using specification for function printf_va_27
-[eva] using specification for function printf_va_28
-[eva] using specification for function printf_va_29
-[eva] using specification for function printf_va_30
-[eva] using specification for function printf_va_31
-[eva] using specification for function printf_va_32
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_initial_stdout.__fc_FILE_id ∈ {1}
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 445fabe655d1672e99748a164372a8a965992194..c17925d4c6c21eecf89043f7282d7dd9a51c8efa 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -23,7 +23,7 @@
Assigning imprecise value to b because of arithmetic operation on addresses.
[eva:alarm] printf_garbled_mix.c:7: Warning:
pointer downcast. assert (unsigned long)b ≤ 2147483647;
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
[eva:garbled-mix:summary]
diff --git a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
index baa6412d4a5b978505a8ecb810d17e1851d42fc4..142e10dc722bcbc745694a6beb6b2151b6fb82a1 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
@@ -8,7 +8,7 @@
[variadic:typing] printf_redefined.i:7: Warning:
Incorrect type for argument 2. The argument will be cast from long to size_t.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
x ∈ {0}
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index ea0427acf1a58a496c767028060ed1e46870942b..04d622d2fc2c752591aafe1c8ff4160cc2fd5df0 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -27,11 +27,10 @@
[variadic] printf_wrong_arity.c:9:
Fallback translation of call printf to a call to the specialized version printf_va_2_fallback_1.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[kernel:annot:missing-spec] printf_wrong_arity.c:9: Warning:
Neither code nor specification for function printf_va_2_fallback_1,
generating default assigns. See -generated-spec-* options for more info
-[eva] using specification for function printf_va_2_fallback_1
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__fc_initial_stdout.__fc_FILE_id ∈ {1}
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index d2d9c9511abba2f36d972b3aeaf2e921d2b08e24..1d78403904cda85aea0ce82caf9e367878e8fa47 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -27,15 +27,11 @@
[variadic] printf_wrong_pointers.c:18:
Translating call to printf to a call to the specialized version printf_va_5.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] printf_wrong_pointers.c:14: Warning:
function printf_va_1: precondition \valid(param0) got status invalid.
-[eva] using specification for function printf_va_2
-[eva] using specification for function printf_va_3
[eva:alarm] printf_wrong_pointers.c:16: Warning:
function printf_va_3: precondition \valid(param0) got status invalid.
-[eva] using specification for function printf_va_4
-[eva] using specification for function printf_va_5
[eva:alarm] printf_wrong_pointers.c:18: Warning:
function printf_va_5: precondition valid_read_wstring(param0) got status invalid.
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 3e2d7c846202217c4e2c91b18884203efa9ce439..bcb991db71837e9e18c800ec19b55567d401f831 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -77,19 +77,7 @@
[variadic:typing] printf_wrong_types.c:36: Warning:
Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
-[eva] using specification for function printf_va_2
-[eva] using specification for function printf_va_3
-[eva] using specification for function printf_va_4
-[eva] using specification for function printf_va_5
-[eva] using specification for function printf_va_6
-[eva] using specification for function printf_va_7
-[eva] using specification for function printf_va_8
-[eva] using specification for function printf_va_9
-[eva] using specification for function printf_va_10
-[eva] using specification for function printf_va_11
-[eva] using specification for function printf_va_12
-[eva] using specification for function printf_va_13
+[eva] using specification for function printf
[eva:alarm] printf_wrong_types.c:30: Warning:
function printf_va_13: precondition valid_read_string(param0) got status invalid.
[eva] ====== VALUES COMPUTED ======
@@ -484,19 +472,7 @@ int main(void)
[variadic:typing] printf_wrong_types.c:36: Warning:
Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function printf_va_1
-[eva] using specification for function printf_va_2
-[eva] using specification for function printf_va_3
-[eva] using specification for function printf_va_4
-[eva] using specification for function printf_va_5
-[eva] using specification for function printf_va_6
-[eva] using specification for function printf_va_7
-[eva] using specification for function printf_va_8
-[eva] using specification for function printf_va_9
-[eva] using specification for function printf_va_10
-[eva] using specification for function printf_va_11
-[eva] using specification for function printf_va_12
-[eva] using specification for function printf_va_13
+[eva] using specification for function printf
[eva:alarm] printf_wrong_types.c:30: Warning:
function printf_va_13: precondition valid_read_string(param0) got status invalid.
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
index 1cc8b6672489b509deaf541592d6f3f95a6d2455..248c50d1d15d7eb7db08258bf8d0e79ec9d2277c 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.0.res.oracle
@@ -30,9 +30,7 @@
[variadic] scanf.c:25:
Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function scanf_va_1
-[eva] using specification for function scanf_va_2
-[eva] using specification for function scanf_va_3
+[eva] using specification for function scanf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
c[0] ∈ [--..--]
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
index 0e55f1c5d201a9af2a1536508d987734e8e52ac0..56f67a3e7e84e7db761315f18b17abc718a90877 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.1.res.oracle
@@ -25,9 +25,7 @@
[variadic] scanf.c:25:
Translating call to scanf to a call to the specialized version scanf_va_4.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function scanf_va_1
-[eva] using specification for function scanf_va_2
-[eva] using specification for function scanf_va_3
+[eva] using specification for function scanf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
c[0] ∈ [--..--]
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index 141acf793645b2ac10cea87ab44af1df01a7a8a1..a7bc2276d8b72d3ada9922e8bb10761ff5605a8e 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -19,7 +19,7 @@
[variadic] scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function scanf_va_1
+[eva] using specification for function scanf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
n ∈ [--..--]
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index 457094451bc48c6506a531c7d10737ad667ec5dc..460100c536fcb2f404427758852b081ed56a3504 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -23,7 +23,7 @@
[eva] Analyzing a complete application starting at main
[eva] FRAMAC_SHARE/libc/string.h:167:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
-[eva] using specification for function snprintf_va_1
+[eva] using specification for function snprintf
[eva] FRAMAC_SHARE/libc/stdio.h:250:
Cannot evaluate range bound format_length(format) - 1
(unsupported ACSL construct: logic function format_length). Approximating
@@ -33,7 +33,6 @@
(0 .. format_length(format) - 1)) got status unknown.
[eva:alarm] snprintf.c:13: Warning:
assertion got status invalid (stopping propagation).
-[eva] using specification for function snprintf_va_2
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
data[0..98] ∈ {65}
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index f395811f0709c44b3765d7ede71beff92d19153d..91a2158738fdc6557ebdfa23a888a44fffb84f7b 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -34,7 +34,7 @@
Translating call to swprintf to a call to the specialized version swprintf_va_2.
[eva] Analyzing a complete application starting at main
[eva] using specification for function wmemset
-[eva] using specification for function swprintf_va_1
+[eva] using specification for function swprintf
[eva] FRAMAC_SHARE/libc/wchar.h:311:
Cannot evaluate range bound wformat_length(format) - 1
(unsupported ACSL construct: logic function wformat_length). Approximating
@@ -44,7 +44,6 @@
(0 .. wformat_length(format) - 1)) got status unknown.
[eva:alarm] swprintf.c:13: Warning:
assertion got status invalid (stopping propagation).
-[eva] using specification for function swprintf_va_2
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
data[0..98] ∈ {65}
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 42d8e77e446bfcd9720dc3c732a3ce578cd463ad..ab7b545ce35b208ef5616bac861bce95dd5d4d8f 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -49,16 +49,10 @@
[variadic] wchar.c:23:
Translating call to swscanf to a call to the specialized version swscanf_va_1.
[eva] Analyzing a complete application starting at main
-[eva] using specification for function wprintf_va_1
-[eva] using specification for function wprintf_va_2
-[eva] using specification for function wprintf_va_3
-[eva] using specification for function wprintf_va_4
-[eva] using specification for function wprintf_va_5
-[eva] using specification for function wprintf_va_6
-[eva] using specification for function swprintf_va_1
-[eva] using specification for function wscanf_va_1
-[eva] using specification for function wscanf_va_2
-[eva] using specification for function swscanf_va_1
+[eva] using specification for function wprintf
+[eva] using specification for function swprintf
+[eva] using specification for function wscanf
+[eva] using specification for function swscanf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
input[0] ∈ {102}
diff --git a/tests/builtins/oracle/linked_list.0.res.oracle b/tests/builtins/oracle/linked_list.0.res.oracle
index 46862a2655e4a39732bfc305d8f565ee8716e9df..c8eb4801d046fc967b389b0d10a46cfc0de3f50e 100644
--- a/tests/builtins/oracle/linked_list.0.res.oracle
+++ b/tests/builtins/oracle/linked_list.0.res.oracle
@@ -2298,7 +2298,7 @@
==END OF DUMP==
[eva] computing for function printf_va_1 <- main.
Called from linked_list.c:51.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] linked_list.c:51: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] linked_list.c:50: starting to merge loop iterations
diff --git a/tests/builtins/oracle/linked_list.1.res.oracle b/tests/builtins/oracle/linked_list.1.res.oracle
index 916c9e2bba809abbcd4abc13454d1183d6998a5a..99d1d200f800f1275ffe31a177ad0e34c6bca413 100644
--- a/tests/builtins/oracle/linked_list.1.res.oracle
+++ b/tests/builtins/oracle/linked_list.1.res.oracle
@@ -804,7 +804,7 @@
==END OF DUMP==
[eva] computing for function printf_va_1 <- main.
Called from linked_list.c:51.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] linked_list.c:51: function printf_va_1: precondition got status valid.
[eva:garbled-mix:assigns] linked_list.c:51:
The specification of function printf_va_1
diff --git a/tests/builtins/oracle/linked_list.2.res.oracle b/tests/builtins/oracle/linked_list.2.res.oracle
index cb6c771649a7abe82835280f67ccf0516a2cd706..cc10e98d65308f40e0804fe6329e734316692d0b 100644
--- a/tests/builtins/oracle/linked_list.2.res.oracle
+++ b/tests/builtins/oracle/linked_list.2.res.oracle
@@ -967,7 +967,7 @@
==END OF DUMP==
[eva] computing for function printf_va_1 <- main.
Called from linked_list.c:51.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] linked_list.c:51: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function printf_va_1 <- main.
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 2c969383f1f633e2d193897191201c7d3822fe32..16e587299fdf5a44dc27df75db6104464318017b 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -94,12 +94,11 @@
[eva] ieee_1180_1990.c:189: starting to merge loop iterations
[eva] computing for function printf_va_1 <- main.
Called from ieee_1180_1990.c:195.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] ieee_1180_1990.c:195: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function printf_va_2 <- main.
Called from ieee_1180_1990.c:196.
-[eva] using specification for function printf_va_2
[eva] ieee_1180_1990.c:196: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function IEEE_1180_1990_mkbk <- main.
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 6d9eacca9b28634179776ed8c0f1e8af2f3a30e5..fac44c24435bd1ec8cef98ad67690d598ba5a466 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/tests/libc/oracle/netdb_c.res.oracle
@@ -173,7 +173,7 @@
[eva] Done for function gai_strerror
[eva] computing for function fprintf_va_1 <- main.
Called from netdb_c.c:36.
-[eva] using specification for function fprintf_va_1
+[eva] using specification for function fprintf
[eva] netdb_c.c:36:
function fprintf_va_1: precondition valid_read_string(param0) got status valid.
[eva] netdb_c.c:36:
@@ -198,7 +198,6 @@
[eva] Done for function close
[eva] computing for function fprintf_va_2 <- main.
Called from netdb_c.c:57.
-[eva] using specification for function fprintf_va_2
[eva] netdb_c.c:57: function fprintf_va_2: precondition got status valid.
[eva] Done for function fprintf_va_2
[eva] computing for function exit <- main.
diff --git a/tests/libc/oracle/netinet_in_h.res.oracle b/tests/libc/oracle/netinet_in_h.res.oracle
index fc01b99309a8d22f6e12912c97e97e6edad7bcaa..ea3b1d86fcc4a6ae6661698467666087fb0b757e 100644
--- a/tests/libc/oracle/netinet_in_h.res.oracle
+++ b/tests/libc/oracle/netinet_in_h.res.oracle
@@ -10,7 +10,7 @@
[eva] Done for function inet_ntoa
[eva] computing for function printf_va_1 <- main.
Called from netinet_in_h.c:6.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] netinet_in_h.c:6:
function printf_va_1: precondition valid_read_string(param0) got status valid.
[eva] netinet_in_h.c:6:
diff --git a/tests/libc/oracle/pthread_h.res.oracle b/tests/libc/oracle/pthread_h.res.oracle
index d2d451907e89b55691ef2169aa49bd1e01e6264e..65333319be6e528f1133b67f364f1087ea70897d 100644
--- a/tests/libc/oracle/pthread_h.res.oracle
+++ b/tests/libc/oracle/pthread_h.res.oracle
@@ -19,7 +19,7 @@
[eva] Done for function pthread_create
[eva] computing for function printf_va_2 <- main.
Called from pthread_h.c:22.
-[eva] using specification for function printf_va_2
+[eva] using specification for function printf
[eva] pthread_h.c:22: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_2 <- main.
@@ -30,7 +30,6 @@
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
Called from pthread_h.c:25.
-[eva] using specification for function printf_va_3
[eva] pthread_h.c:25: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function pthread_setname_np <- main.
@@ -47,7 +46,6 @@
[eva] Done for function pthread_getname_np
[eva] computing for function printf_va_4 <- main.
Called from pthread_h.c:30.
-[eva] using specification for function printf_va_4
[eva:alarm] pthread_h.c:30: Warning:
function printf_va_4: precondition valid_read_string(param0) got status unknown.
[eva] pthread_h.c:30:
@@ -57,7 +55,6 @@
Called from pthread_h.c:35.
[eva] computing for function printf_va_1 <- start_routine <- main.
Called from pthread_h.c:11.
-[eva] using specification for function printf_va_1
[eva] pthread_h.c:11: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] Recording results for start_routine
@@ -70,7 +67,6 @@
[eva] Done for function pthread_join
[eva] computing for function printf_va_5 <- main.
Called from pthread_h.c:39.
-[eva] using specification for function printf_va_5
[eva] pthread_h.c:39: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
[eva] computing for function printf_va_5 <- main.
@@ -83,7 +79,6 @@
out of bounds read. assert \valid_read(retv);
[eva] computing for function printf_va_6 <- main.
Called from pthread_h.c:42.
-[eva] using specification for function printf_va_6
[eva] pthread_h.c:42: function printf_va_6: precondition got status valid.
[eva] Done for function printf_va_6
[eva] Recording results for main
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index 29be464b5cb944c6368d69e519dedbaa55c31176..f3a24652dc25a198f18e79333b456cd0b9cff435 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -48,7 +48,7 @@
out of bounds read. assert \valid_read((struct element **)node);
[eva] computing for function fprintf_va_1 <- main.
Called from search_h.c:36.
-[eva] using specification for function fprintf_va_1
+[eva] using specification for function fprintf
[eva] search_h.c:36: function fprintf_va_1: precondition got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- main.
diff --git a/tests/libc/oracle/socket.0.res.oracle b/tests/libc/oracle/socket.0.res.oracle
index de9e0f72d413ad09b208ca4739816223a752a7e1..50dd89548c6bc593549fdcb08abc9a45f821964f 100644
--- a/tests/libc/oracle/socket.0.res.oracle
+++ b/tests/libc/oracle/socket.0.res.oracle
@@ -17,7 +17,7 @@
[eva] Done for function socketpair
[eva] computing for function fprintf_va_1 <- init_sockets <- main.
Called from socket.c:52.
-[eva] using specification for function fprintf_va_1
+[eva] using specification for function fprintf
[eva] socket.c:52: function fprintf_va_1: precondition got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- init_sockets <- main.
@@ -55,7 +55,7 @@
[eva] Done for function read
[eva] computing for function printf_va_1 <- test_read <- main.
Called from socket.c:62.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] socket.c:62: Warning:
function printf_va_1: precondition valid_read_string(param0) got status unknown.
[eva] socket.c:62:
@@ -83,7 +83,6 @@
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_2 <- test_readv <- main.
Called from socket.c:75.
-[eva] using specification for function printf_va_2
[eva:alarm] socket.c:75: Warning:
function printf_va_2: precondition valid_read_nstring(param0, 2) got status unknown.
[eva:alarm] socket.c:75: Warning:
@@ -113,7 +112,6 @@
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_3 <- test_recvmsg <- main.
Called from socket.c:95.
-[eva] using specification for function printf_va_3
[eva:alarm] socket.c:95: Warning:
function printf_va_3: precondition valid_read_nstring(param0, 2) got status unknown.
[eva:alarm] socket.c:95: Warning:
diff --git a/tests/libc/oracle/socket.1.res.oracle b/tests/libc/oracle/socket.1.res.oracle
index 2d2f6878bba16e4f9b93d4ee980002127e25faf2..ed8486ee0b606634c5f9c06adacd1cd64acc8459 100644
--- a/tests/libc/oracle/socket.1.res.oracle
+++ b/tests/libc/oracle/socket.1.res.oracle
@@ -17,7 +17,7 @@
[eva] Done for function socketpair
[eva] computing for function fprintf_va_1 <- init_sockets <- main.
Called from socket.c:52.
-[eva] using specification for function fprintf_va_1
+[eva] using specification for function fprintf
[eva] socket.c:52: function fprintf_va_1: precondition got status valid.
[eva] Done for function fprintf_va_1
[eva] computing for function exit <- init_sockets <- main.
@@ -55,7 +55,7 @@
[eva] Done for function read
[eva] computing for function printf_va_1 <- test_read <- main.
Called from socket.c:62.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] socket.c:62: Warning:
function printf_va_1: precondition valid_read_string(param0) got status unknown.
[eva] socket.c:62:
@@ -83,7 +83,6 @@
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_2 <- test_readv <- main.
Called from socket.c:75.
-[eva] using specification for function printf_va_2
[eva:alarm] socket.c:75: Warning:
function printf_va_2: precondition valid_read_nstring(param0, 2) got status unknown.
[eva:alarm] socket.c:75: Warning:
@@ -113,7 +112,6 @@
assert \initialized((char *)rcv_buffer_scattered1);
[eva] computing for function printf_va_3 <- test_recvmsg <- main.
Called from socket.c:95.
-[eva] using specification for function printf_va_3
[eva:alarm] socket.c:95: Warning:
function printf_va_3: precondition valid_read_nstring(param0, 2) got status unknown.
[eva:alarm] socket.c:95: Warning:
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 04ce3cdeaf2eb25346dd838eb2ff86a512987a2d..c1ee6d4f4e1635d8ab62aa87e0b6c6d86938e498 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -120,7 +120,7 @@
accessing uninitialized left-value. assert \initialized(&child_pid);
[eva] computing for function printf_va_1 <- main.
Called from spawn_h.c:101.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] spawn_h.c:101: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function waitpid <- main.
@@ -131,29 +131,24 @@
[eva] Done for function waitpid
[eva] computing for function printf_va_2 <- main.
Called from spawn_h.c:110.
-[eva] using specification for function printf_va_2
[eva] spawn_h.c:110: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva:alarm] spawn_h.c:111: Warning:
accessing uninitialized left-value. assert \initialized(&status);
[eva] computing for function printf_va_3 <- main.
Called from spawn_h.c:112.
-[eva] using specification for function printf_va_3
[eva] spawn_h.c:112: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function printf_va_4 <- main.
Called from spawn_h.c:114.
-[eva] using specification for function printf_va_4
[eva] spawn_h.c:114: function printf_va_4: precondition got status valid.
[eva] Done for function printf_va_4
[eva] computing for function printf_va_5 <- main.
Called from spawn_h.c:116.
-[eva] using specification for function printf_va_5
[eva] spawn_h.c:116: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
[eva] computing for function printf_va_6 <- main.
Called from spawn_h.c:118.
-[eva] using specification for function printf_va_6
[eva] spawn_h.c:118: function printf_va_6: precondition got status valid.
[eva] Done for function printf_va_6
[eva] spawn_h.c:105: starting to merge loop iterations
diff --git a/tests/libc/oracle/stdio_c.res.oracle b/tests/libc/oracle/stdio_c.res.oracle
index 7d6dcd1f44cb49b980d3ac6e3295f19220f24991..1ea318fc100fb63bc53b33d63c62a24c9e628530 100644
--- a/tests/libc/oracle/stdio_c.res.oracle
+++ b/tests/libc/oracle/stdio_c.res.oracle
@@ -244,7 +244,7 @@
[eva] Done for function asprintf
[eva] computing for function printf_va_1 <- main.
Called from stdio_c.c:33.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] stdio_c.c:33: Warning:
function printf_va_1: precondition valid_read_string(param0) got status unknown.
[eva] stdio_c.c:33:
diff --git a/tests/libc/oracle/stdio_h.res.oracle b/tests/libc/oracle/stdio_h.res.oracle
index f74af6c62a036f1b3cfeda344edb88b30fa5e759..501e3cbf6721700b16630e39626ebf133fa82927 100644
--- a/tests/libc/oracle/stdio_h.res.oracle
+++ b/tests/libc/oracle/stdio_h.res.oracle
@@ -86,7 +86,7 @@
[eva] Done for function freopen
[eva] computing for function printf_va_1 <- main.
Called from stdio_h.c:36.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] stdio_h.c:36: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function fclose <- main.
@@ -146,7 +146,6 @@
accessing uninitialized left-value. assert \initialized(&s);
[eva] computing for function printf_va_2 <- main.
Called from stdio_h.c:60.
-[eva] using specification for function printf_va_2
[eva:alarm] stdio_h.c:60: Warning:
function printf_va_2: precondition valid_read_string(param0) got status invalid.
[eva] stdio_h.c:60:
@@ -180,7 +179,6 @@
assert ¬\dangling(&s_0);
[eva] computing for function printf_va_3 <- main.
Called from stdio_h.c:71.
-[eva] using specification for function printf_va_3
[eva:alarm] stdio_h.c:71: Warning:
function printf_va_3: precondition valid_read_string(param0) got status invalid.
[eva] stdio_h.c:71:
diff --git a/tests/saveload/oracle/bool_sav.res b/tests/saveload/oracle/bool_sav.res
index 841511fc87a2dcce6c5a66411451c944d11ff628..56bc2f79e2b49468deba7a536cd033e01b9187a7 100644
--- a/tests/saveload/oracle/bool_sav.res
+++ b/tests/saveload/oracle/bool_sav.res
@@ -14,27 +14,23 @@
[eva] Done for function f
[eva] computing for function printf_va_1 <- main.
Called from bool.c:29.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] bool.c:29: function printf_va_1: precondition got status valid.
[eva] Done for function printf_va_1
[eva] computing for function printf_va_2 <- main.
Called from bool.c:31.
-[eva] using specification for function printf_va_2
[eva] bool.c:31: function printf_va_2: precondition got status valid.
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main.
Called from bool.c:33.
-[eva] using specification for function printf_va_3
[eva] bool.c:33: function printf_va_3: precondition got status valid.
[eva] Done for function printf_va_3
[eva] computing for function printf_va_4 <- main.
Called from bool.c:35.
-[eva] using specification for function printf_va_4
[eva] bool.c:35: function printf_va_4: precondition got status valid.
[eva] Done for function printf_va_4
[eva] computing for function printf_va_5 <- main.
Called from bool.c:37.
-[eva] using specification for function printf_va_5
[eva] bool.c:37: function printf_va_5: precondition got status valid.
[eva] Done for function printf_va_5
[eva] Recording results for main
diff --git a/tests/slicing/oracle/use_spec.1.res.oracle b/tests/slicing/oracle/use_spec.1.res.oracle
index a31502ad99e2832eb3faabd36931f827124eb3f2..b1ca4b07028b2107c706608a320d58db806b81f0 100644
--- a/tests/slicing/oracle/use_spec.1.res.oracle
+++ b/tests/slicing/oracle/use_spec.1.res.oracle
@@ -51,11 +51,10 @@
G2 ∈ {0}
[eva] computing for function h_slice_2 <- main2.
Called from use_spec.i:38.
-[eva] using specification for function h_slice_2
+[eva] using specification for function h
[eva] Done for function h_slice_2
[eva] computing for function h_slice_1 <- main2.
Called from use_spec.i:40.
-[eva] using specification for function h_slice_1
[eva] Done for function h_slice_1
[eva:alarm] use_spec.i:41: Warning:
signed overflow. assert -2147483648 ≤ tmp + G2;
diff --git a/tests/syntax/oracle/string_concat.res.oracle b/tests/syntax/oracle/string_concat.res.oracle
index 7ed5facee899a0ee3fdd471f2a5f7b445943f818..672e70fb40eaba58c89016436dcab9af7d07a4a7 100644
--- a/tests/syntax/oracle/string_concat.res.oracle
+++ b/tests/syntax/oracle/string_concat.res.oracle
@@ -3,7 +3,7 @@
[eva:initial-state] Values of globals at initialization
test[0..65535] ∈ {97}
[65536] ∈ {0}
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__retres ∈ {0}
diff --git a/tests/syntax/oracle/wstring_concat.res.oracle b/tests/syntax/oracle/wstring_concat.res.oracle
index a61c7bee287e308d9dd1cfe59e51b31b20da64b5..6f978c9b82ffb7fbe703354fbec0a598938c5757 100644
--- a/tests/syntax/oracle/wstring_concat.res.oracle
+++ b/tests/syntax/oracle/wstring_concat.res.oracle
@@ -3,7 +3,7 @@
[eva:initial-state] Values of globals at initialization
test[0..65535] ∈ {97}
[65536] ∈ {0}
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
__retres ∈ {0}
diff --git a/tests/value/oracle/cast.res.oracle b/tests/value/oracle/cast.res.oracle
index 3d7f2bdc46af05d80381e823a9163f5cb5f871d7..8f632c2773cef859c8d46ca7f93fa46520c0885b 100644
--- a/tests/value/oracle/cast.res.oracle
+++ b/tests/value/oracle/cast.res.oracle
@@ -29,7 +29,7 @@
[eva] Done for function any_int_4
[eva] computing for function printf_va_1 <- main1 <- main.
Called from cast.i:46.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] cast.i:46: Warning:
function printf_va_1: precondition got status unknown.
[eva] Done for function printf_va_1
@@ -39,7 +39,6 @@
Called from cast.i:74.
[eva] computing for function printf_va_2 <- main2 <- main.
Called from cast.i:67.
-[eva] using specification for function printf_va_2
[eva:alarm] cast.i:67: Warning:
function printf_va_2: precondition got status unknown.
[eva] Done for function printf_va_2
@@ -55,7 +54,6 @@
[eva] Done for function printf_va_2
[eva] computing for function printf_va_3 <- main2 <- main.
Called from cast.i:69.
-[eva] using specification for function printf_va_3
[eva:alarm] cast.i:69: Warning:
function printf_va_3: precondition got status unknown.
[eva] Done for function printf_va_3
diff --git a/tests/value/oracle/cert_exp35_c.res.oracle b/tests/value/oracle/cert_exp35_c.res.oracle
index b4d301d74c4e6c2f66bcb8188c2945d4f474fe3c..c98fec494d33cfaf6cb37f6c16546b2edd8270b2 100644
--- a/tests/value/oracle/cert_exp35_c.res.oracle
+++ b/tests/value/oracle/cert_exp35_c.res.oracle
@@ -11,7 +11,7 @@
[eva] Done for function addressee
[eva] computing for function printf_va_1 <- main.
Called from cert_exp35_c.i:24.
-[eva] using specification for function printf_va_1
+[eva] using specification for function printf
[eva:alarm] cert_exp35_c.i:24: Warning:
function printf_va_1: precondition valid_read_string(param0) got status unknown.
[eva:alarm] cert_exp35_c.i:24: Warning: