From 6a126ee84bb0ff73cbfa9c2fabe9f8ec53723565 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 25 Oct 2017 07:34:05 +0200
Subject: [PATCH] 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 | 2 +-
src/plugins/e-acsl/dup_functions.ml | 12 +++++++++++-
src/plugins/e-acsl/env.mli | 4 ++++
3 files changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 6ae3346abd6..13e442dcf12 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 373e519ccb7..d5854b2b8a8 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 44e3e5a7225..965b5e89d68 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 ->
--
GitLab