[Eva] use vorig_name in feedback to minimize noise due to Variadic renaming

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;

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:
   

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.

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

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}

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" }}

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}

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}

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] 

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}

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}

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 ======

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 ======

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] ∈ [--..--]

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] ∈ [--..--]

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 ∈ [--..--]

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}

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}

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}

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