[variadic] avoid transforming function type of otherwise untouched builtins

src/plugins/aorai/tests/ya/oracle/serial.res.oracle

 [kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/ya/serial.c:79: Warning: 
-  Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
 [aorai] Welcome to the Aorai plugin
 [kernel:annot:missing-spec] tests/ya/serial.c:43: Warning: 
   Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
@@ -299,7 +297,7 @@
   100% of the logical properties reached have been proven.
   ----------------------------------------------------------------------------
 [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:176: Warning: 
+[kernel:typing:implicit-function-declaration] TMPDIR/aorai_serial_0.i:174: Warning: 
   Calling undeclared function Frama_C_interval. Old style K&R code?
 /* Generated by Frama-C */
 enum aorai_States {
@@ -338,13 +336,11 @@ enum aorai_OpStatusList {
     aorai_Terminated = 1,
     aorai_Called = 0
 };
+/* compiler builtin: 
+   void Frama_C_show_aorai_state(...);   */
 int volatile indefinitely;
 int buffer[5];
 int n = 0;
-/*@ assigns \result;
-    assigns \result \from \nothing; */
-extern int Frama_C_show_aorai_state(void);
-
 /*@ ghost enum aorai_ListOper aorai_CurOperation; */
 /*@ ghost enum aorai_OpStatusList aorai_CurOpStatus; */
 /*@ ghost int aorai_CurStates = Wait1; */

src/plugins/variadic/classify.ml

@@ -110,6 +110,20 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
 (* Classification                                                           *)
 (* ************************************************************************ *)
 
+let is_frama_c_builtin name =
+  Ast_info.is_frama_c_builtin name ||
+  Cil_builtins.Builtin_functions.mem name ||
+  Extlib.string_prefix "__FRAMAC_" name (* Mthread prefixes *)
+
+let va_builtins = [
+  "__builtin_va_start";
+  "__builtin_va_copy";
+  "__builtin_va_arg";
+  "__builtin_va_end";
+]
+
+let is_va_builtin s = List.mem s va_builtins
+
 let classify_std env vi = match vi.vname with
   (* fcntl.h - Overloads of functions *)
   | "fcntl" -> mk_overload env
@@ -149,7 +163,8 @@ let classify_std env vi = match vi.vname with
   (* stropts.h *)
   | "ioctl"   -> mk_overload env ["__va_ioctl_void" ; "__va_ioctl_int" ; "__va_ioctl_ptr"]
   | n when Extlib.string_prefix "__sync_" n -> Misc
-  | n when Cil_builtins.Builtin_functions.mem n -> Builtin
+  | n when is_va_builtin n -> Misc
+  | n when is_frama_c_builtin n -> Builtin
   (* Anything else *)
   | _ -> Unknown
 

src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle

@@ -2,6 +2,8 @@
   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.
+[variadic] tests/erroneous/variadic-builtin.i:5: 
+  Call to variadic builtin Frama_C_show_each_warning left untransformed.
 [kernel] tests/erroneous/variadic-builtin.i:6: Plug-in variadic aborted: unimplemented feature.
   You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
   '[Plug-in variadic] The variadic plugin doesn't handle calls to a pointer to the variadic builtin Frama_C_show_each_warning.'.

src/plugins/variadic/translate.ml

@@ -27,17 +27,7 @@ module Typ = Extends.Typ
 
 (* List of builtin function names to translate *)
 
-let va_builtins = [
-  "__builtin_va_start";
-  "__builtin_va_copy";
-  "__builtin_va_arg";
-  "__builtin_va_end"]
-
-let is_framac_builtin vi =
-  Ast_info.is_frama_c_builtin vi.vname ||
-  Cil_builtins.Builtin_functions.mem vi.vname ||
-  Extlib.string_prefix "__FRAMAC_" vi.vname (* Mthread prefixes *)
-
+let is_framac_builtin vi = Classify.is_frama_c_builtin vi.vname
 
 (* In place visitor for translation *)
 
@@ -89,13 +79,14 @@ let translate_variadics (file : file) =
       begin match glob with
         | GFunDecl(_, vi, _) ->
           (match Table.find_opt classification vi with
-           | None -> ()
+           | None -> Cil.DoChildren (* may transform the type *)
            | Some { vf_class = Builtin } ->
              Self.result ~level:2 ~current:true
                "Variadic builtin %s left untransformed." vi.vname;
+             Cil.SkipChildren
            | Some _ ->
-             Generic.add_vpar vi);
-          Cil.DoChildren
+             Generic.add_vpar vi;
+             Cil.DoChildren)
 
         | GFun ({svar = vi} as fundec, _) ->
           if Table.mem classification vi then begin
@@ -147,7 +138,10 @@ let translate_variadics (file : file) =
             | Overload o -> Standard.overloaded_call ~fundec o
             | Aggregator a -> Standard.aggregator_call ~fundec ~ghost a
             | FormatFun f -> Standard.format_fun_call ~fundec env f
-            | Builtin -> raise Not_found
+            | Builtin ->
+              Self.result ~level:2 ~current:true
+                "Call to variadic builtin %s left untransformed." f.vname;
+              raise Not_found
             | _ -> raise Standard.Translate_call_exn
           in
           call_translator block loc mk_call vf args
@@ -157,7 +151,7 @@ let translate_variadics (file : file) =
       in
       begin match i with
         | Call(_, {enode = Lval(Var vi, _)}, _, _)
-          when List.mem vi.vname va_builtins ->
+          when Classify.is_va_builtin vi.vname ->
           File.must_recompute_cfg fundec;
           Cil.ChangeTo (Generic.translate_va_builtin fundec i)
         | Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->