diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 6ae3346abd606df4a038fb4b4bc27edb5f5b81f3..13e442dcf120bb4e0d2a62f178a3169072d6c782 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -66,10 +66,10 @@ PLUGIN_CMO:= local_config \
 	gmpz \
 	literal_strings \
 	mmodel_analysis \
-	dup_functions \
 	exit_points \
 	label \
 	env \
+	dup_functions \
 	interval \
 	typing \
 	quantif \
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 373e519ccb7fb41d5b266ebf99addab045e75902..d5854b2b8a823281b3454aefbf04fb3c5536fb92 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -160,7 +160,17 @@ let dup_funspec tbl bhv spec =
 let dup_fundec loc spec bhv kf vi new_vi =
   new_vi.vdefined <- true;
   let formals = Kernel_function.get_formals kf in
-  let new_formals = List.map (fun vi -> Cil.copyVarinfo vi vi.vname) formals in
+  let mk_formal vi =
+    let name =
+      if vi.vname = "" then
+        Env.Varname.get ~scope:Env.Function
+          (Misc.mk_gen_name "unamed_formal")
+      else
+        vi.vname
+    in
+    Cil.copyVarinfo vi name
+  in
+  let new_formals = List.map mk_formal formals in
   let res =
     let ty = Kernel_function.get_return_type kf in
     if Cil.isVoidType ty then None
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 44e3e5a722541c8a89ed27bcb7b78e5fd11edeb9..965b5e89d6868ff57ff2d2a8147d368b9e02587e 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -41,6 +41,10 @@ type scope =
   | Function
   | Local_block
 
+module Varname: sig
+  val get: scope:scope -> string -> string
+end
+
 val new_var:
   loc:location -> ?init:bool -> ?scope:scope -> ?name:string ->
   t -> term option -> typ ->