[eacsl] Don't process Variadic generated functions

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -639,6 +639,9 @@ let inject_in_global (env, main) = function
     env, main
   | g when Rtl.Symbols.mem_global g ->
     env, main
+  (* generated function declaration: nothing to do *)
+  | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
+    env, main
 
   (* variable declarations *)
   | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->

src/plugins/e-acsl/src/libraries/misc.ml

@@ -36,6 +36,9 @@ let is_fc_or_compiler_builtin vi =
    let prefix = String.sub vi.vname 0 prefix_length in
    Datatype.String.equal prefix "__builtin_")
 
+let is_fc_stdlib_generated vi =
+  Cil.hasAttribute "fc_stdlib_generated" vi.vattr
+
 (* ************************************************************************** *)
 (** {2 Handling \result} *)
 (* ************************************************************************** *)

src/plugins/e-acsl/src/libraries/misc.mli

@@ -40,6 +40,10 @@ val result_vi: kernel_function -> varinfo
 
 val is_fc_or_compiler_builtin: varinfo -> bool
 
+val is_fc_stdlib_generated: varinfo -> bool
+(** Returns true if the [varinfo] is a generated stdlib function. (For instance
+    generated function by the Variadic plug-in. *)
+
 val term_addr_of: loc:location -> term_lval -> typ -> term
 
 val cty: logic_type -> typ

src/plugins/e-acsl/src/project_initializer/prepare_ast.ml

@@ -392,6 +392,8 @@ let must_duplicate kf vi =
   not (is_variadic_function vi)
   && (* it is not a built-in *)
   not (Misc.is_fc_or_compiler_builtin vi)
+  && (* it is not a generated function *)
+  not (Misc.is_fc_stdlib_generated vi)
   &&
   ((* either explicitely listed as to be not instrumented *)
     not (Functions.instrument kf)