[variadic] do not translate registered builtin functions

src/plugins/variadic/classify.ml

@@ -148,7 +148,7 @@ 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 Cil_builtins.Builtin_functions.mem n -> Builtin
   (* Anything else *)
   | _ -> Unknown
 

src/plugins/variadic/translate.ml

@@ -35,6 +35,7 @@ let va_builtins = [
 
 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 *)
 
 
@@ -147,6 +148,7 @@ 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
             | _ -> raise Standard.Translate_call_exn
           in
           call_translator block loc mk_call vf args

src/plugins/variadic/va_types.mli

@@ -26,6 +26,8 @@ open Cil_types
 type variadic_class =
   | Unknown
   (** Function declared and not known by Frama-C *)
+  | Builtin
+  (** Function registered as a builtin function in Cil_builtins *)
   | Defined
   (** Function for which we have the definition in the project *)
   | Misc