Use allocate_objects to manage new symbol creation

This simplifies the code in generate_nondet_init and reduces code
duplication.

Author: antlechner

src/util/nondet.cpp

@@ -7,6 +7,7 @@ Author: Diffblue Ltd.
 \*******************************************************************/
 
 #include "nondet.h"
+#include "allocate_objects.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -16,25 +17,17 @@ Author: Diffblue Ltd.
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
   const exprt &max_value_expr,
-  const std::string &name_prefix,
   const std::string &basename_prefix,
-  const irep_idt &mode,
   const source_locationt &source_location,
-  symbol_table_baset &symbol_table,
+  allocate_objectst &allocate_objects,
   code_blockt &instructions)
 {
   PRECONDITION(min_value_expr.type() == max_value_expr.type());
   const typet &int_type = min_value_expr.type();
 
   // Declare a symbol for the non deterministic integer.
-  const symbol_exprt &nondet_symbol = get_fresh_aux_symbol(
-                                        int_type,
-                                        name_prefix,
-                                        basename_prefix,
-                                        source_location,
-                                        mode,
-                                        symbol_table)
-                                        .symbol_expr();
+  const symbol_exprt &nondet_symbol =
+    allocate_objects.allocate_automatic_local_object(int_type, basename_prefix);
   instructions.add(code_declt(nondet_symbol));
 
   // Assign the symbol any non deterministic integer value.
@@ -58,23 +51,19 @@ symbol_exprt generate_nondet_int(
 symbol_exprt generate_nondet_int(
   const mp_integer &min_value,
   const mp_integer &max_value,
-  const std::string &name_prefix,
   const std::string &basename_prefix,
   const typet &int_type,
-  const irep_idt &mode,
   const source_locationt &source_location,
-  symbol_table_baset &symbol_table,
+  allocate_objectst &allocate_objects,
   code_blockt &instructions)
 {
   PRECONDITION(min_value < max_value);
   return generate_nondet_int(
     from_integer(min_value, int_type),
     from_integer(max_value, int_type),
-    name_prefix,
     basename_prefix,
-    mode,
     source_location,
-    symbol_table,
+    allocate_objects,
     instructions);
 }
 
@@ -93,15 +82,16 @@ code_blockt generate_nondet_switch(
 
   code_blockt result_block;
 
+  allocate_objectst allocate_objects(
+    mode, source_location, name_prefix, symbol_table);
+
   const symbol_exprt &switch_value = generate_nondet_int(
     0,
     switch_cases.size() - 1,
-    id2string(name_prefix),
     "nondet_int",
     int_type,
-    mode,
     source_location,
-    symbol_table,
+    allocate_objects,
     result_block);
 
   code_blockt switch_block;

src/util/nondet.h

@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H
 #define CPROVER_JAVA_BYTECODE_NONDET_H
 
+#include <util/allocate_objects.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -26,11 +27,9 @@ Author: Diffblue Ltd.
 symbol_exprt generate_nondet_int(
   const exprt &min_value_expr,
   const exprt &max_value_expr,
-  const std::string &name_prefix,
   const std::string &basename_prefix,
-  const irep_idt &mode,
   const source_locationt &source_location,
-  symbol_table_baset &symbol_table,
+  allocate_objectst &allocate_objects,
   code_blockt &instructions);
 
 /// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
@@ -42,26 +41,22 @@ symbol_exprt generate_nondet_int(
 /// ```
 /// \param min_value: Minimum value (inclusive) of returned int.
 /// \param max_value: Maximum value (inclusive) of returned int.
-/// \param name_prefix: Prefix for the fresh symbol name generated (should be
-///   function id)
+/// \param basename_prefix: Basename prefix for the fresh symbol name generated.
 /// \param int_type: The type of the int used to non-deterministically choose
 ///   one of the switch cases.
-/// \param mode: Mode (language) of the symbol to be generated.
+/// \param allocate_objects: Handles allocation of new objects.
 /// \param source_location: The location to mark the generated int with.
-/// \param symbol_table: The global symbol table.
 /// \param [out] instructions: Output instructions are written to
 ///   'instructions'. These declare, nondet-initialise and range-constrain (with
 ///   assume statements) a fresh integer.
 /// \return Returns a symbol expression for the resulting integer.
 symbol_exprt generate_nondet_int(
   const mp_integer &min_value,
   const mp_integer &max_value,
-  const std::string &name_prefix,
   const std::string &basename_prefix,
   const typet &int_type,
-  const irep_idt &mode,
   const source_locationt &source_location,
-  symbol_table_baset &symbol_table,
+  allocate_objectst &allocate_objects,
   code_blockt &instructions);
 
 typedef std::vector<codet> alternate_casest;