Merge branch 'julien/bugfix/bts2303' into 'master'

fix bts bug #2303 about unamed formals (cannot be easily tested through an execu…

See merge request !168

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 \

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.

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

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 ->