diff --git a/src/plugins/variadic/environment.ml b/src/plugins/variadic/environment.ml
index 77cbd5aa164e25b86baa964fd344662d60f772d2..e561d19a840790e654362ed126dcde9c1018556b 100644
--- a/src/plugins/variadic/environment.ml
+++ b/src/plugins/variadic/environment.ml
@@ -90,6 +90,12 @@ let find_type (env : t) (namespace : Logic_typing.type_namespace)
| Logic_typing.Enum ->
TEnum (find_enum env tname, [])
+let mem_global (env : t) (vname : string) : bool =
+ Table.mem env.globals vname
+
+let mem_function (env : t) (vname : string) : bool =
+ Table.mem env.functions vname
+
let from_file (file : file) : t =
let env = empty () in
let v = object inherit Cil.nopCilVisitor
diff --git a/src/plugins/variadic/environment.mli b/src/plugins/variadic/environment.mli
index 9163b7b16cd5b49637fd03b67f358667a0a92c28..d8e54a24f77c9bf0ff48d574824ef0823fa820d1 100644
--- a/src/plugins/variadic/environment.mli
+++ b/src/plugins/variadic/environment.mli
@@ -34,3 +34,6 @@ val find_struct : t -> string -> Cil_types.compinfo
val find_union : t -> string -> Cil_types.compinfo
val find_enum : t -> string -> Cil_types.enuminfo
val find_type : t -> Logic_typing.type_namespace -> string -> Cil_types.typ
+
+val mem_global : t -> string -> bool
+val mem_function : t -> string -> bool
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index ae07bb0df4ee365492332fda2d4447e169dc0137..366a587f94f596452fb982aca1898b06d3db61ba 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -173,23 +173,34 @@ let match_call ~builder new_callee new_tparams args =
Build.(List.iter pure (of_exp_list unused_args));
Build.(translated_call (var new_callee) (of_exp_list new_args))
+
+let check_available_name env name =
+ not @@ Environment.mem_global env name
+ && not @@ Environment.mem_function env name
+
+let get_next_name env id name =
+ let rec aux id =
+ let next_name = name ^ (string_of_int id) in
+ if check_available_name env next_name then
+ next_name, id
+ else
+ aux (id + 1)
+ in
+ aux id
+
(* ************************************************************************ *)
(* Fallback calls *)
(* ************************************************************************ *)
-let fallback_fun_call ~builder ~callee vf args =
+let fallback_fun_call ~builder ~callee env vf args =
let module Build = (val builder : Builder.S) in
(* Choose function name *)
let name = callee.vname in
let vorig_name = callee.vorig_name in
- let count =
- try Fallback_counts.find name
- with Not_found -> 0
- in
- let count = count + 1 in
- Fallback_counts.replace name count;
- let new_name = name ^ "_fallback_" ^ (string_of_int count) in
+ let count = try Fallback_counts.find name + 1 with Not_found -> 1 in
+ let new_name, new_count = get_next_name env count (name ^ "_fallback_") in
+ Fallback_counts.replace name new_count;
(* Start building the function *)
let loc = vf.vf_decl.vdecl in
@@ -431,15 +442,15 @@ let valid_read_nstring typ =
let format_length typ =
find_predicate_by_width typ "format_length" "wformat_length"
-
let build_specialized_fun ~builder env vf format_fun tvparams =
let open Format_types in
let module Build = (val builder : Builder.S) in
(* Choose function name *)
let name = vf.vf_decl.vorig_name in
- vf.vf_specialization_count <- vf.vf_specialization_count + 1;
- let new_name = name ^ "_va_" ^ (string_of_int vf.vf_specialization_count) in
+ let id = vf.vf_specialization_count + 1 in
+ let new_name, new_count = get_next_name env id (name ^ "_va_") in
+ vf.vf_specialization_count <- new_count;
(* Start building the function *)
let loc = vf.vf_decl.vdecl in
diff --git a/src/plugins/variadic/standard.mli b/src/plugins/variadic/standard.mli
index d06853851d9238bfbf47d01bc44c6d52398957b8..f7350aa4a112e9a89ef42eb1ba96199b3d1cfbce 100644
--- a/src/plugins/variadic/standard.mli
+++ b/src/plugins/variadic/standard.mli
@@ -24,6 +24,7 @@ exception Translate_call_exn of Cil_types.varinfo
val fallback_fun_call :
builder:Builder.t -> callee:Cil_types.varinfo ->
+ Environment.t ->
Va_types.variadic_function -> Cil_types.exp list -> unit
val aggregator_call :
diff --git a/src/plugins/variadic/tests/known/oracle/print_libc.pretty.c b/src/plugins/variadic/tests/known/oracle/print_libc.pretty.c
index 0cc4de0588c6eab6ff596070c679cf5526386811..c90642f461962fdde63bb01ed6d90757cddd1c7d 100644
--- a/src/plugins/variadic/tests/known/oracle/print_libc.pretty.c
+++ b/src/plugins/variadic/tests/known/oracle/print_libc.pretty.c
@@ -51,12 +51,12 @@ int printf_va_1(char const * restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
-int printf_va_1(char const * restrict format);
+int printf_va_2(char const * restrict format);
int main(void)
{
int __retres;
- printf(""); /* printf_va_1 */
+ printf(""); /* printf_va_2 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 21489606b074ca1cb2089786424f090d02fd1457..95778a48f085fb1313b855c324d699fcbae8d43d 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -200,7 +200,7 @@ let translate_variadics (file : file) =
try
f ~builder args
with Standard.Translate_call_exn callee ->
- Standard.fallback_fun_call ~callee ~builder vf args
+ Standard.fallback_fun_call ~callee ~builder env vf args
in
match vf.vf_class with
| Overload o -> cover_failure (Standard.overloaded_call o vf)
diff --git a/tests/syntax/oracle/variadic_fresh_names.res.oracle b/tests/syntax/oracle/variadic_fresh_names.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1fb230dff45abd65517f9051ac02522c249c33fa
--- /dev/null
+++ b/tests/syntax/oracle/variadic_fresh_names.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing variadic_fresh_names.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param0);
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+ int param0);
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param0);
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_2(FILE * restrict stream, char const * restrict format,
+ int param0);
+
+void main(void)
+{
+ fprintf(__fc_stderr,"%d ",42); /* fprintf_va_2 */
+ return;
+}
+
+
diff --git a/tests/syntax/variadic_fresh_names.c b/tests/syntax/variadic_fresh_names.c
new file mode 100644
index 0000000000000000000000000000000000000000..46615262b2d8bdc38fdafb9b32a4b4b5a65296fa
--- /dev/null
+++ b/tests/syntax/variadic_fresh_names.c
@@ -0,0 +1,24 @@
+/* run.config
+PLUGIN: variadic
+STDOPT:
+*/
+#include "stdio.h"
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param0);
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..))), param0;
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+ int param0);
+
+void main(void)
+{
+ fprintf(__fc_stderr,"%d ",42); /* fprintf_va_1 */
+ return;
+}