diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 75ec65a7b495488bd454bdf700317ad3e6ad505b..b3d6c65a3d604eafb6a8c631dc38c1d826b51f16 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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, _) ->
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 2c123e74461384011d02b51f0066aa6f1ba157df..7aafe514878534d25ce09b762a60bcf8db7776a0 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/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} *)
 (* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 090b237753110e5e1561cf6e1e336d818833937b..f5a2c28359790d6d6cd4a9285b30c3333944bebe 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/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
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 2f167b55c03dbf9eb5fc203cdc93d569dfcd8323..fd41f2f344dc9176642685d12ab897de4626ffbc 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/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)