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 348e8c477dabbdd59001acfa7a657eb14cb7aa1b..a5caa303321a2c8a59eeca0aa1e0fd1d70baad98 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 3cecd8f9b1e42365b8af2c9e3217c941bd59aea4..3ba86d9da3ae971fb31c76d3bfd3a967be0ddb5c 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 46f76bbce8ef2dcfe72df9f3cce29d8fce2d54a5..b2bbd04dbb1302f8de40b034909dbbebf1b1b46f 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, _) ->