From 992d082c2b5e09fe42339eb4ed5981ef496b1bbd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 25 Oct 2017 16:03:47 +0200
Subject: [PATCH] comment for previous bug fix
---
src/plugins/e-acsl/dup_functions.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index d5854b2b8a8..9d330878ff3 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -163,6 +163,8 @@ let dup_fundec loc spec bhv kf vi new_vi =
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
--
GitLab