From 0082360e812da01ab7e0f2c4b09ac852711891e0 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 26 Sep 2024 10:50:17 +0200
Subject: [PATCH] [Eva] use vorig_name in feedback to minimize noise due to
Variadic renaming
---
src/plugins/eva/engine/compute_functions.ml | 4 ++-
.../redefine_anonymous_parameters.res.oracle | 2 +-
.../tests/known/oracle/exec.res.oracle | 2 +-
.../tests/known/oracle/fcntl.res.oracle | 3 +-
.../tests/known/oracle/open.res.oracle | 2 +-
.../tests/known/oracle/open_wrong.res.oracle | 2 +-
.../tests/known/oracle/openat.res.oracle | 2 +-
.../tests/known/oracle/printf.res.oracle | 34 +------------------
.../oracle/printf_garbled_mix.res.oracle | 2 +-
.../known/oracle/printf_redefined.res.oracle | 2 +-
.../oracle/printf_wrong_arity.res.oracle | 3 +-
.../oracle/printf_wrong_pointers.res.oracle | 6 +---
.../oracle/printf_wrong_types.res.oracle | 28 ++-------------
.../tests/known/oracle/scanf.0.res.oracle | 4 +--
.../tests/known/oracle/scanf.1.res.oracle | 4 +--
.../tests/known/oracle/scanf_loop.res.oracle | 2 +-
.../tests/known/oracle/snprintf.res.oracle | 3 +-
.../tests/known/oracle/swprintf.res.oracle | 3 +-
.../tests/known/oracle/wchar.res.oracle | 14 +++-----
.../builtins/oracle/linked_list.0.res.oracle | 2 +-
.../builtins/oracle/linked_list.1.res.oracle | 2 +-
.../builtins/oracle/linked_list.2.res.oracle | 2 +-
tests/idct/oracle/ieee_1180_1990.res.oracle | 3 +-
tests/libc/oracle/netdb_c.res.oracle | 3 +-
tests/libc/oracle/netinet_in_h.res.oracle | 2 +-
tests/libc/oracle/pthread_h.res.oracle | 7 +---
tests/libc/oracle/search_h.res.oracle | 2 +-
tests/libc/oracle/socket.0.res.oracle | 6 ++--
tests/libc/oracle/socket.1.res.oracle | 6 ++--
tests/libc/oracle/spawn_h.res.oracle | 7 +---
tests/libc/oracle/stdio_c.res.oracle | 2 +-
tests/libc/oracle/stdio_h.res.oracle | 4 +--
tests/saveload/oracle/bool_sav.res | 6 +---
tests/slicing/oracle/use_spec.1.res.oracle | 3 +-
tests/syntax/oracle/string_concat.res.oracle | 2 +-
tests/syntax/oracle/wstring_concat.res.oracle | 2 +-
tests/value/oracle/cast.res.oracle | 4 +--
tests/value/oracle/cert_exp35_c.res.oracle | 2 +-
38 files changed, 46 insertions(+), 143 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index fd44697b05b..5941a06f123 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 0c1758790c3..ea61b8a1a4d 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 03338e671a1..1da3a3b77a3 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 b15b13096bc..9448251dd8b 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 ec407450fca..89c49a920e7 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 ae94f9c59c8..338a8d81ada 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 e45e5dc8e07..89a7c668900 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 a567cee9c48..a4bc497d251 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 445fabe655d..c17925d4c6c 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 baa6412d4a5..142e10dc722 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 ea0427acf1a..04d622d2fc2 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 d2d9c9511ab..1d78403904c 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 3e2d7c84620..bcb991db718 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 1cc8b667248..248c50d1d15 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 0e55f1c5d20..56f67a3e7e8 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 141acf79364..a7bc2276d8b 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 457094451bc..460100c536f 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 f395811f070..91a2158738f 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 42d8e77e446..ab7b545ce35 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 46862a2655e..c8eb4801d04 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 916c9e2bba8..99d1d200f80 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 cb6c771649a..cc10e98d653 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 2c969383f1f..16e587299fd 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 6d9eacca9b2..fac44c24435 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 fc01b99309a..ea3b1d86fcc 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 d2d451907e8..65333319be6 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 29be464b5cb..f3a24652dc2 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 de9e0f72d41..50dd89548c6 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 2d2f6878bba..ed8486ee0b6 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 04ce3cdeaf2..c1ee6d4f4e1 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 7d6dcd1f44c..1ea318fc100 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 f74af6c62a0..501e3cbf672 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 841511fc87a..56bc2f79e2b 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 a31502ad99e..b1ca4b07028 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 7ed5facee89..672e70fb40e 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 a61c7bee287..6f978c9b82f 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 3d7f2bdc46a..8f632c2773c 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 b4d301d74c4..c98fec494d3 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:
--
GitLab