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/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 989c3f5c6d845bbcce1374ed72462d75454c8af1..b080ed4c2a5a8b2c1632a6076814833e951b74ae 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,27 +15,31 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/10/25] Fix bug #2303 about unnamed formals in
+	        annotated functions.
+-  E-ACSL       [2017/06/10] Add --free-valid-address option to e-acsl.gcc.sh
+-  E-ACSL       [2017/05/29] Add --fail-with-code option to e-acsl.gcc.sh
+-  E-ACSL       [2017/05/19] Add --temporal option to e-acsl.gcc.sh
+-  E-ACSL       [2017/05/19] New detection of temporal errors in E-ACSL
+	        through -e-acsl-temporal-validity (disabled by default)
+-  E-ACSL       [2017/03/26] Add --weak-validity option to e-acsl.gcc.sh
+-  E-ACSL       [2017/03/26] Add --rt-verbose option to e-acsl.gcc.sh
+-  E-ACSL       [2017/03/26] Add --keep-going option to e-acsl.gcc.sh allowing
+	        a program to continue execution after an assertion failure
+-  E-ACSL       [2017/03/26] Add --stack-size and --heap-size options to
+	        e-acsl-gcc.sh allowing to change the default sizes of the
+	        respective shadow spaces
+
 #################################
 Plugin E-ACSL Phosphorus-20170515
 #################################
 
--! E-ACSL       [2017/06/10] Add --free-valid-address option to e-acsl.gcc.sh
--! E-ACSL       [2017/05/29] Add --fail-with-code option to e-acsl.gcc.sh
--! E-ACSL       [2017/05/19] Add --temporal option to e-acsl.gcc.sh
--! E-ACSL       [2017/05/19] Enable analysis for temporal errors in E-ACSL
--! E-ACSL       [2017/03/26] Add --weak-validity option to e-acsl.gcc.sh
--! E-ACSL       [2017/03/26] Add --rt-verbose option to e-acsl.gcc.sh
--! E-ACSL       [2017/03/26] Add --keep-going option to e-acsl.gcc.sh allowing
-	        a program to continue execution after an assertion failure
--! E-ACSL       [2017/03/26] Add --stack-size and --heap-size options to
-	        e-acsl-gcc.sh allowing to change the default sizes of the
-	        respective shadow spaces
 -  E-ACSL       [2017/03/29] The (much more efficient) shadow memory model is
 	        now used by default.
 -* E-ACSL       [2017/03/28] Fix backtrace when the failed instrumented programs
 	        do not require memory model.
 -! E-ACSL       [2017/03/19] Remove --print|-p option from e-acsl-gcc.sh
--! E-ACSL       [2017/03/16] Add --check option to e-acsl-gcc.sh which allows
+-  E-ACSL       [2017/03/16] Add --check option to e-acsl-gcc.sh which allows
 	        to check the integrity of the generated AST before
 	        instrumentation.
 -! E-ACSL       [2017/03/03] Remove precond rte option from e-acsl-gss.sh.
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 373e519ccb7fb41d5b266ebf99addab045e75902..9d330878ff321b82be59f130950bb863b3eb7ff5 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -160,7 +160,19 @@ 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
+        (* unamed formal parameter: must generate a fresh name since a fundec
+           cannot have unnamed formals (see bts #2303). *)
+        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 ->