C and Java nondet factories: use unique symbol names

The nondet symbol factory uses "tmp" as a default basename prefix, and
in all other places already generated unique names using
`get_fresh_aux_symbol`. This function, however, will happily use exactly
that basename when there wouldn't be a conflict. The code fixed in this
commit, however, did not yet use this facility, and just assumed that
each parameter of the target function would result in a unique local
name. A parameter named "tmp," then, resulted in a conflict.
Consistently using `get_fresh_aux_symbol` addresses this problem.

Fixes: #6566

Co-authored-by: Matthias Güdemann <[email protected]>

fixup! C nondet factory: Ensure parameter initialisers use unique symbol names

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
+#include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/nondet_bool.h>
 #include <util/prefix.h>
@@ -1551,24 +1552,18 @@ exprt object_factory(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &log)
 {
-  irep_idt identifier=id2string(goto_functionst::entry_point())+
-    "::"+id2string(base_name);
-
-  auxiliary_symbolt main_symbol;
-  main_symbol.mode=ID_java;
-  main_symbol.is_static_lifetime=false;
-  main_symbol.name=identifier;
-  main_symbol.base_name=base_name;
-  main_symbol.type=type;
-  main_symbol.location=loc;
+  const symbolt &main_symbol = get_fresh_aux_symbol(
+    type,
+    id2string(goto_functionst::entry_point()),
+    id2string(base_name),
+    loc,
+    ID_java,
+    symbol_table);
+
   parameters.function_id = goto_functionst::entry_point();
 
   exprt object=main_symbol.symbol_expr();
 
-  symbolt *main_symbol_ptr;
-  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  CHECK_RETURN(!moving_symbol_failed);
-
   java_object_factoryt state(
     loc, parameters, symbol_table, pointer_type_selector, log);
   code_blockt assignments;
@@ -1583,7 +1578,7 @@ exprt object_factory(
     update_in_placet::NO_UPDATE_IN_PLACE,
     loc);
 
-  state.add_created_symbol(main_symbol_ptr);
+  state.add_created_symbol(&main_symbol);
   state.declare_created_symbols(init_code);
 
   assert_type_consistency(assignments);

regression/cbmc/pointer-function-parameters/main.c

@@ -0,0 +1,3 @@
+void f(int *b, int tmp)
+{
+}

regression/cbmc/pointer-function-parameters/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function f
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -15,6 +15,7 @@ Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/fresh_symbol.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
 #include <util/pointer_expr.h>
@@ -204,23 +205,15 @@ symbol_exprt c_nondet_symbol_factory(
   const c_object_factory_parameterst &object_factory_parameters,
   const lifetimet lifetime)
 {
-  irep_idt identifier=id2string(goto_functionst::entry_point())+
-    "::"+id2string(base_name);
-
-  auxiliary_symbolt main_symbol;
-  main_symbol.mode=ID_C;
-  main_symbol.is_static_lifetime=false;
-  main_symbol.name=identifier;
-  main_symbol.base_name=base_name;
-  main_symbol.type=type;
-  main_symbol.location=loc;
-
+  const symbolt &main_symbol = get_fresh_aux_symbol(
+    type,
+    id2string(goto_functionst::entry_point()),
+    id2string(base_name),
+    loc,
+    ID_C,
+    symbol_table);
   symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
 
-  symbolt *main_symbol_ptr;
-  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  CHECK_RETURN(!moving_symbol_failed);
-
   symbol_factoryt state(
     symbol_table,
     loc,
@@ -231,7 +224,7 @@ symbol_exprt c_nondet_symbol_factory(
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 
-  state.add_created_symbol(main_symbol_ptr);
+  state.add_created_symbol(&main_symbol);
   state.declare_created_symbols(init_code);
 
   init_code.append(assignments);