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

fix bts bug #2303 about unamed formals (cannot be easily tested through an executable program that prints the issue)

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

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