From f276cd9c8ac77d769abc116cfc9dfca8e651fb62 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 7 Jan 2021 17:29:02 +0100
Subject: [PATCH] [variadic] only emit "untransformed" message for builtins
that are variadic.
---
.../tests/erroneous/oracle/variadic-builtin.res.oracle | 2 ++
.../tests/known/oracle/printf_garbled_mix.res.oracle | 2 --
src/plugins/variadic/translate.ml | 6 ++++--
3 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index 348e8c477da..a5caa303321 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -1,3 +1,5 @@
+[variadic] tests/erroneous/variadic-builtin.i:1:
+ Declaration of variadic function Frama_C_show_each_warning.
[variadic] tests/erroneous/variadic-builtin.i:1:
Variadic builtin Frama_C_show_each_warning left untransformed.
[kernel] tests/erroneous/variadic-builtin.i:6: Plug-in variadic aborted: unimplemented feature.
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 3cecd8f9b1e..3ba86d9da3a 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
@@ -14,8 +14,6 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:541:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_garbled_mix.c:8:
- Variadic builtin Frama_C_show_each_nb_printed left untransformed.
[variadic] tests/known/printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
[eva] Analyzing a complete application starting at main
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 46f76bbce8e..b2bbd04dbb1 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -89,8 +89,10 @@ let translate_variadics (file : file) =
method! vglob glob =
begin match glob with
| GFunDecl(_, vi, _) when is_framac_builtin vi ->
- Self.result ~level:2 ~current:true
- "Variadic builtin %s left untransformed." vi.vname;
+ if Classify.classify env vi <> None then begin
+ Self.result ~level:2 ~current:true
+ "Variadic builtin %s left untransformed." vi.vname;
+ end;
Cil.SkipChildren
| GFunDecl(_, vi, _) ->
--
GitLab