From b4260dd61e6d733af55d881577c1e97f03473023 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 20 Jun 2018 14:11:29 +0100
Subject: [PATCH 01/14] Add missing const's and move's

Add const keyword at the declaration of variables that will not get
modified.
In some case, we inline them instead to avoid declaration, when
declaration doesn't add value.
In other cases, we don't make the variable const but use move where it
is used.

fixup! Add missing const's
---
 .../java_string_library_preprocess.cpp        | 204 +++++++++---------
 1 file changed, 102 insertions(+), 102 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 9cd208b9860..927b816eef8 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -277,10 +277,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
 {
   exprt::operandst ops;
   for(const auto &p : params)
-  {
-    symbol_exprt sym(p.get_identifier(), p.type());
-    ops.push_back(sym);
-  }
+    ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
   return process_operands(ops, loc, symbol_table, init_code);
 }
 
@@ -372,7 +369,7 @@ java_string_library_preprocesst::process_equals_function_operands(
   // TODO: Manage the case where we have a non-String Object (this should
   // probably be handled upstream. At any rate, the following code should be
   // protected with assertions on the type of op1.
-  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
+  const typecast_exprt tcast(op1, to_pointer_type(op0.type()));
   ops.push_back(
     convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
   return ops;
@@ -451,21 +448,21 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
   code_blockt &code)
 {
   // array is *array_pointer
-  dereference_exprt array=
+  const dereference_exprt array =
     checked_dereference(array_pointer, array_pointer.type().subtype());
   // array_data is array_pointer-> data
   const exprt array_data = get_data(array, symbol_table);
-  symbolt sym_char_array = get_fresh_aux_symbol(
+  const symbolt &sym_char_array = get_fresh_aux_symbol(
     array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
-  symbol_exprt char_array=sym_char_array.symbol_expr();
+  const symbol_exprt char_array = sym_char_array.symbol_expr();
   // char_array = array_pointer->data
   code.add(code_assignt(char_array, array_data), loc);
 
   // string_expr is `{ rhs->length; string_array }`
-  refined_string_exprt string_expr(
+  const refined_string_exprt string_expr(
     get_length(array, symbol_table), char_array, refined_string_type);
 
-  dereference_exprt inf_array(
+  const dereference_exprt inf_array(
     char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
 
   add_pointer_to_array_association(
@@ -502,25 +499,26 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  symbolt sym_length = get_fresh_aux_symbol(
+  const symbolt &sym_length = get_fresh_aux_symbol(
     index_type,
     "cprover_string_length",
     "cprover_string_length",
     loc,
     ID_java,
     symbol_table);
-  symbol_exprt length_field=sym_length.symbol_expr();
-  pointer_typet array_type = pointer_type(java_char_type());
-  symbolt sym_content = get_fresh_aux_symbol(
+  const symbol_exprt length_field = sym_length.symbol_expr();
+  const pointer_typet array_type = pointer_type(java_char_type());
+  const symbolt &sym_content = get_fresh_aux_symbol(
     array_type,
     "cprover_string_content",
     "cprover_string_content",
     loc,
     ID_java,
     symbol_table);
-  symbol_exprt content_field = sym_content.symbol_expr();
+  const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
-  refined_string_exprt str(length_field, content_field, refined_string_type);
+  const refined_string_exprt str{
+    length_field, content_field, refined_string_type};
   code.add(code_declt(length_field), loc);
   return str;
 }
@@ -544,10 +542,10 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
 
-  exprt nondet_array_expr =
+  const exprt nondet_array_expr =
     make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
 
-  address_of_exprt array_pointer(
+  const address_of_exprt array_pointer(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
@@ -575,7 +573,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  exprt str=fresh_string(type, loc, symbol_table);
+  const exprt str = fresh_string(type, loc, symbol_table);
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
@@ -602,9 +600,10 @@ static codet code_assign_function_application(
   const exprt::operandst &arguments,
   symbol_table_baset &symbol_table)
 {
-  exprt fun_app=make_function_application(
-    function_name, arguments, lhs.type(), symbol_table);
-  return code_assignt(lhs, fun_app);
+  return code_assignt(
+    lhs,
+    make_function_application(
+      function_name, arguments, lhs.type(), symbol_table));
 }
 
 /// return the result of a function call
@@ -622,9 +621,8 @@ codet java_string_library_preprocesst::code_return_function_application(
   const typet &type,
   symbol_table_baset &symbol_table)
 {
-  exprt fun_app=make_function_application(
-    function_name, arguments, type, symbol_table);
-  return code_returnt(fun_app);
+  return code_returnt(
+    make_function_application(function_name, arguments, type, symbol_table));
 }
 
 /// Declare a fresh symbol of type array of character with infinite size.
@@ -674,14 +672,14 @@ void add_pointer_to_array_association(
 {
   PRECONDITION(array.type().id() == ID_array);
   PRECONDITION(pointer.type().id() == ID_pointer);
-  symbolt &return_sym = get_fresh_aux_symbol(
+  const symbolt &return_sym = get_fresh_aux_symbol(
     java_int_type(),
     "return_array",
     "return_array",
     loc,
     ID_java,
     symbol_table);
-  auto return_expr = return_sym.symbol_expr();
+  const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
     code_assign_function_application(
@@ -706,7 +704,7 @@ void add_array_to_length_association(
   const source_locationt &loc,
   code_blockt &code)
 {
-  symbolt &return_sym = get_fresh_aux_symbol(
+  const symbolt &return_sym = get_fresh_aux_symbol(
     java_int_type(),
     "return_array",
     "return_array",
@@ -743,7 +741,7 @@ void add_character_set_constraint(
   code_blockt &code)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
-  symbolt &return_sym = get_fresh_aux_symbol(
+  const symbolt &return_sym = get_fresh_aux_symbol(
     java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
@@ -781,7 +779,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code_blockt &code)
 {
   // int return_code;
-  symbolt return_code_sym = get_fresh_aux_symbol(
+  const symbolt &return_code_sym = get_fresh_aux_symbol(
     java_int_type(),
     std::string("return_code_") + function_name.c_str(),
     std::string("return_code_") + function_name.c_str(),
@@ -961,14 +959,14 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   code_blockt code;
 
   // Declaring and allocating String * str
-  exprt str = allocate_fresh_string(
+  const exprt str = allocate_fresh_string(
     type.return_type(), loc, function_id, symbol_table, code);
 
   // Expression representing 0.0
-  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
+  const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
   ieee_floatt zero_float(float_spec);
   zero_float.from_float(0.0);
-  constant_exprt zero=zero_float.to_expr();
+  const constant_exprt zero = zero_float.to_expr();
 
   // For each possible case with have a condition and a string_exprt
   std::vector<exprt> condition_list;
@@ -976,7 +974,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Case of computerized scientific notation
   condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
-  refined_string_exprt sci_notation = string_expr_of_function(
+  const refined_string_exprt sci_notation = string_expr_of_function(
     ID_cprover_string_of_float_scientific_notation_func,
     {arg},
     loc,
@@ -986,9 +984,9 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Subcase of negative scientific notation
   condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
-  refined_string_exprt minus_sign =
+  const refined_string_exprt minus_sign =
     string_literal_to_string_expr("-", loc, symbol_table, code);
-  refined_string_exprt neg_sci_notation = string_expr_of_function(
+  const refined_string_exprt neg_sci_notation = string_expr_of_function(
     ID_cprover_string_concat_func,
     {minus_sign, sci_notation},
     loc,
@@ -998,20 +996,20 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Case of NaN
   condition_list.push_back(isnan_exprt(arg));
-  refined_string_exprt nan =
+  const refined_string_exprt nan =
     string_literal_to_string_expr("NaN", loc, symbol_table, code);
   string_expr_list.push_back(nan);
 
   // Case of Infinity
   extractbit_exprt is_neg(arg, float_spec.width()-1);
   condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
-  refined_string_exprt infinity =
+  const refined_string_exprt infinity =
     string_literal_to_string_expr("Infinity", loc, symbol_table, code);
   string_expr_list.push_back(infinity);
 
   // Case -Infinity
   condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
-  refined_string_exprt minus_infinity =
+  const refined_string_exprt minus_infinity =
     string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
   string_expr_list.push_back(minus_infinity);
 
@@ -1022,25 +1020,24 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);
   bound_sup_float.change_spec(float_spec);
-  constant_exprt bound_inf=bound_inf_float.to_expr();
-  constant_exprt bound_sup=bound_sup_float.to_expr();
+  const constant_exprt bound_inf = bound_inf_float.to_expr();
+  const constant_exprt bound_sup = bound_sup_float.to_expr();
 
-  and_exprt is_simple_float(
-    binary_relation_exprt(arg, ID_ge, bound_inf),
-    binary_relation_exprt(arg, ID_lt, bound_sup));
+  const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
+                                  binary_relation_exprt(arg, ID_lt, bound_sup)};
   condition_list.push_back(is_simple_float);
 
-  refined_string_exprt simple_notation = string_expr_of_function(
+  const refined_string_exprt simple_notation = string_expr_of_function(
     ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
   string_expr_list.push_back(simple_notation);
 
   // Case of a negative number in simple notation
-  and_exprt is_neg_simple_float(
+  const and_exprt is_neg_simple_float{
     binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
-    binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup)));
+    binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
   condition_list.push_back(is_neg_simple_float);
 
-  refined_string_exprt neg_simple_notation = string_expr_of_function(
+  const refined_string_exprt neg_simple_notation = string_expr_of_function(
     ID_cprover_string_concat_func,
     {minus_sign, simple_notation},
     loc,
@@ -1107,10 +1104,11 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
   code_blockt code;
 
   // Processing parameters
-  exprt::operandst args=process_parameters(params, loc, symbol_table, code);
+  const exprt::operandst args =
+    process_parameters(params, loc, symbol_table, code);
 
   // string_expr <- function(arg1)
-  refined_string_exprt string_expr =
+  const refined_string_exprt string_expr =
     string_expr_of_function(function_name, args, loc, symbol_table, code);
 
   // arg_this <- string_expr
@@ -1137,7 +1135,7 @@ java_string_library_preprocesst::make_assign_and_return_function_from_call(
   symbol_table_baset &symbol_table)
 {
   // This is similar to assign functions except we return a pointer to `this`
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params.empty());
   PRECONDITION(!params[0].get_identifier().empty());
   code_blockt code;
@@ -1246,10 +1244,10 @@ java_string_library_preprocesst::get_primitive_value_of_object(
   DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive");
 
   // declare tmp_type_name to hold the value
-  std::string aux_name="tmp_"+id2string(type_name);
-  symbolt symbol=get_fresh_aux_symbol(
+  const std::string aux_name = "tmp_" + id2string(type_name);
+  const symbolt &symbol = get_fresh_aux_symbol(
     value_type, aux_name, aux_name, loc, ID_java, symbol_table);
-  auto value = symbol.symbol_expr();
+  const auto value = symbol.symbol_expr();
 
   // Check that the type of the object is in the symbol table,
   // otherwise there is no safe way of finding its value.
@@ -1263,10 +1261,11 @@ java_string_library_preprocesst::get_primitive_value_of_object(
       struct_type.get_component("value");
     if(!value_comp.is_nil())
     {
-      pointer_typet pointer_type=::pointer_type(struct_type);
-      dereference_exprt deref(
-        typecast_exprt(object, pointer_type), pointer_type.subtype());
-      member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
+      const pointer_typet struct_pointer_type = pointer_type(struct_type);
+      dereference_exprt deref{typecast_exprt(object, struct_pointer_type),
+                              struct_pointer_type.subtype()};
+      const member_exprt deref_value{
+        std::move(deref), value_comp.get_name(), value_comp.type()};
       code.add(code_assignt(value, deref_value), loc);
       return value;
     }
@@ -1290,14 +1289,14 @@ dereference_exprt java_string_library_preprocesst::get_object_at_index(
   const exprt &argv,
   std::size_t index)
 {
-  dereference_exprt deref_objs(argv, argv.type().subtype());
-  pointer_typet empty_pointer = pointer_type(java_void_type());
-  pointer_typet pointer_of_pointer=pointer_type(empty_pointer);
-  member_exprt data_member(deref_objs, "data", pointer_of_pointer);
-  plus_exprt data_pointer_plus_index(
-    data_member, from_integer(index, java_int_type()), data_member.type());
-  return dereference_exprt(
-    data_pointer_plus_index, data_pointer_plus_index.type().subtype());
+  const dereference_exprt deref_objs{argv, argv.type().subtype()};
+  const pointer_typet empty_pointer = pointer_type(java_void_type());
+  const pointer_typet pointer_of_pointer = pointer_type(empty_pointer);
+  const member_exprt data_member{deref_objs, "data", pointer_of_pointer};
+  const plus_exprt data_pointer_plus_index{
+    data_member, from_integer(index, java_int_type()), data_member.type()};
+  return dereference_exprt{data_pointer_plus_index,
+                           data_pointer_plus_index.type().subtype()};
 }
 
 /// Helper for format function. Adds code:
@@ -1352,7 +1351,7 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
     if(name!="string_expr")
     {
       std::string tmp_name="tmp_"+id2string(name);
-      symbolt field_symbol = get_fresh_aux_symbol(
+      const symbolt &field_symbol = get_fresh_aux_symbol(
         type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
       auto field_symbol_expr = field_symbol.symbol_expr();
       field_expr = field_symbol_expr;
@@ -1367,15 +1366,15 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
   }
 
   // arg_i = argv[index]
-  exprt obj=get_object_at_index(argv, index);
-  symbolt object_symbol = get_fresh_aux_symbol(
+  const exprt obj = get_object_at_index(argv, index);
+  const symbolt &object_symbol = get_fresh_aux_symbol(
     obj.type(),
     id2string(function_id),
     "tmp_format_obj",
     loc,
     ID_java,
     symbol_table);
-  symbol_exprt arg_i=object_symbol.symbol_expr();
+  const symbol_exprt arg_i = object_symbol.symbol_expr();
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
@@ -1402,9 +1401,9 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
 
     if(name=="string_expr")
     {
-      pointer_typet string_pointer =
+      const pointer_typet string_pointer =
         java_reference_type(struct_tag_typet("java::java.lang.String"));
-      typecast_exprt arg_i_as_string(arg_i, string_pointer);
+      const typecast_exprt arg_i_as_string{arg_i, string_pointer};
       code_assign_java_string_to_string_expr(
         to_string_expr(field_expr),
         arg_i_as_string,
@@ -1477,9 +1476,9 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
       make_argument_for_format(
         args[1], i, structured_type, loc, function_id, symbol_table, code));
 
-  refined_string_exprt string_expr = string_expr_of_function(
+  const refined_string_exprt string_expr = string_expr_of_function(
     ID_cprover_string_format_func, processed_args, loc, symbol_table, code);
-  exprt java_string = allocate_fresh_string(
+  const exprt java_string = allocate_fresh_string(
     type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1517,22 +1516,21 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
   code_blockt code;
 
   // > Class class1;
-  pointer_typet class_type=
-    java_reference_type(
-      symbol_table.lookup_ref("java::java.lang.Class").type);
-  symbolt class1_sym=get_fresh_aux_symbol(
+  const pointer_typet class_type =
+    java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
+  const symbolt &class1_sym = get_fresh_aux_symbol(
     class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
-  symbol_exprt class1=class1_sym.symbol_expr();
+  const symbol_exprt class1 = class1_sym.symbol_expr();
   code.add(code_declt(class1), loc);
 
   // class_identifier is this->@class_identifier
-  member_exprt class_identifier(
+  const member_exprt class_identifier(
     checked_dereference(this_obj, this_obj.type().subtype()),
     "@class_identifier",
     string_typet());
 
   // string_expr = cprover_string_literal(this->@class_identifier)
-  refined_string_exprt string_expr = string_expr_of_function(
+  const refined_string_exprt string_expr = string_expr_of_function(
     ID_cprover_string_literal_func,
     {class_identifier},
     loc,
@@ -1541,7 +1539,7 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
 
   // string_expr1 = substr(string_expr, 6)
   // We do this to remove the "java::" prefix
-  refined_string_exprt string_expr1 = string_expr_of_function(
+  const refined_string_exprt string_expr1 = string_expr_of_function(
     ID_cprover_string_substring_func,
     {string_expr, from_integer(6, java_int_type())},
     loc,
@@ -1549,9 +1547,9 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
     code);
 
   // string1 = (String*) string_expr
-  pointer_typet string_ptr_type=java_reference_type(
-    symbol_table.lookup_ref("java::java.lang.String").type);
-  exprt string1 = allocate_fresh_string(
+  const pointer_typet string_ptr_type =
+    java_reference_type(symbol_table.lookup_ref("java::java.lang.String").type);
+  const exprt string1 = allocate_fresh_string(
     string_ptr_type, loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1591,8 +1589,8 @@ code_blockt java_string_library_preprocesst::make_function_from_call(
   symbol_table_baset &symbol_table)
 {
   code_blockt code;
-  exprt::operandst args=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  const exprt::operandst args =
+    process_parameters(type.parameters(), loc, symbol_table, code);
   code.add(
     code_return_function_application(
       function_name, args, type.return_type(), symbol_table),
@@ -1624,15 +1622,15 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
   code_blockt code;
 
   // Calling the function
-  exprt::operandst arguments=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  const exprt::operandst arguments =
+    process_parameters(type.parameters(), loc, symbol_table, code);
 
   // String expression that will hold the result
-  refined_string_exprt string_expr =
+  const refined_string_exprt string_expr =
     string_expr_of_function(function_name, arguments, loc, symbol_table, code);
 
   // Assign to string
-  exprt str = allocate_fresh_string(
+  const exprt str = allocate_fresh_string(
     type.return_type(), loc, function_name, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1668,17 +1666,18 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
   code_blockt code;
 
   // String expression that will hold the result
-  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    decl_string_expr(loc, symbol_table, code);
 
   // Assign the argument to string_expr
-  java_method_typet::parametert op = type.parameters()[0];
+  const java_method_typet::parametert &op = type.parameters()[0];
   PRECONDITION(!op.get_identifier().empty());
-  symbol_exprt arg0(op.get_identifier(), op.type());
+  const symbol_exprt arg0{op.get_identifier(), op.type()};
   code_assign_java_string_to_string_expr(
     string_expr, arg0, loc, symbol_table, code);
 
   // Allocate and assign the string
-  exprt str = allocate_fresh_string(
+  const exprt str = allocate_fresh_string(
     type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
@@ -1714,18 +1713,19 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
   code_blockt code;
 
   // String expression that will hold the result
-  refined_string_exprt string_expr = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt string_expr =
+    decl_string_expr(loc, symbol_table, code);
 
   // Assign argument to a string_expr
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params[0].get_identifier().empty());
   PRECONDITION(!params[1].get_identifier().empty());
-  symbol_exprt arg1(params[1].get_identifier(), params[1].type());
+  const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
   code_assign_java_string_to_string_expr(
     string_expr, arg1, loc, symbol_table, code);
 
   // Assign string_expr to `this` object
-  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
+  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
   code.add(
     code_assign_string_expr_to_java_string(
       arg_this, string_expr, symbol_table, true),
@@ -1753,10 +1753,10 @@ code_returnt java_string_library_preprocesst::make_string_length_code(
 {
   (void)function_id;
 
-  java_method_typet::parameterst params = type.parameters();
+  const java_method_typet::parameterst &params = type.parameters();
   PRECONDITION(!params[0].get_identifier().empty());
-  symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
-  dereference_exprt deref =
+  const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
+  const dereference_exprt deref =
     checked_dereference(arg_this, arg_this.type().subtype());
 
   code_returnt ret(get_length(deref, symbol_table));

From 8b791e13c34c938c2548fb5f9ab3309c5c872d99 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 13:19:00 +0000
Subject: [PATCH 02/14] Add function_id parameter to
 convert_exprt_to_string_exprt

This is in preparation to giving the function_id to the function
generating fresh java symbols.
---
 .../java_string_library_preprocess.cpp        | 82 ++++++++++---------
 .../java_string_library_preprocess.h          |  2 +
 .../convert_exprt_to_string_exprt.cpp         |  8 +-
 3 files changed, 50 insertions(+), 42 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 927b816eef8..54f5caae3c7 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -286,6 +286,7 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
 ///   sequence
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
+/// \param function_id: name of the function in which the code will be added
 /// \param init_code: code block, in which declaration will be added:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// char *cprover_string_content;
@@ -300,6 +301,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
   const exprt &expr_to_process,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
+  const irep_idt &function_id,
   code_blockt &init_code)
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
@@ -332,7 +334,8 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   {
     if(implements_java_char_sequence_pointer(p.type()))
       ops.push_back(
-        convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
+        convert_exprt_to_string_exprt(
+          p, loc, symbol_table, loc.get_function(), init_code));
     else if(is_java_char_array_pointer_type(p.type()))
       ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
     else
@@ -364,14 +367,16 @@ java_string_library_preprocesst::process_equals_function_operands(
   PRECONDITION(implements_java_char_sequence_pointer(op0.type()));
 
   ops.push_back(
-    convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
+    convert_exprt_to_string_exprt(
+      op0, loc, symbol_table, loc.get_function(), init_code));
 
   // TODO: Manage the case where we have a non-String Object (this should
   // probably be handled upstream. At any rate, the following code should be
   // protected with assertions on the type of op1.
   const typecast_exprt tcast(op1, to_pointer_type(op0.type()));
   ops.push_back(
-    convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
+    convert_exprt_to_string_exprt(
+      tcast, loc, symbol_table, loc.get_function(), init_code));
   return ops;
 }
 
@@ -587,42 +592,42 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
 
 /// assign the result of a function call
 /// \param lhs: an expression
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: a list of arguments
 /// \param symbol_table: a symbol table
 /// \return the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// lhs = <function_name>(arguments)
+/// lhs = <function_id>(arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 static codet code_assign_function_application(
   const exprt &lhs,
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   symbol_table_baset &symbol_table)
 {
   return code_assignt(
     lhs,
     make_function_application(
-      function_name, arguments, lhs.type(), symbol_table));
+      function_id, arguments, lhs.type(), symbol_table));
 }
 
 /// return the result of a function call
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: a list of arguments
 /// \param type: the return type
 /// \param symbol_table: a symbol table
 /// \return the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// return <function_name>(arguments)
+/// return <function_id>(arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 codet java_string_library_preprocesst::code_return_function_application(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   const typet &type,
   symbol_table_baset &symbol_table)
 {
   return code_returnt(
-    make_function_application(function_name, arguments, type, symbol_table));
+    make_function_application(function_id, arguments, type, symbol_table));
 }
 
 /// Declare a fresh symbol of type array of character with infinite size.
@@ -756,10 +761,10 @@ void add_character_set_constraint(
 }
 
 /// Create a refined_string_exprt `str` whose content and length are fresh
-/// symbols, calls the string primitive with name `function_name`.
+/// symbols, calls the string primitive with name `function_id`.
 /// In the arguments of the primitive `str` takes the place of the result and
 /// the following arguments are given by parameter `arguments.
-/// \param function_name: the name of the function
+/// \param function_id: the name of the function
 /// \param arguments: arguments of the function
 /// \param loc: source location
 /// \param symbol_table: symbol table
@@ -768,11 +773,11 @@ void add_character_set_constraint(
 /// int return_code;
 /// int str.length;
 /// char str.data[str.length]
-/// return_code = <function_name>(str.length, str.data, arguments)
+/// return_code = <function_id>(str.length, str.data, arguments)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// \return refined string expression `str`
 refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const exprt::operandst &arguments,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
@@ -781,8 +786,8 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   // int return_code;
   const symbolt &return_code_sym = get_fresh_aux_symbol(
     java_int_type(),
-    std::string("return_code_") + function_name.c_str(),
-    std::string("return_code_") + function_name.c_str(),
+    std::string("return_code_") + function_id.c_str(),
+    std::string("return_code_") + function_id.c_str(),
     loc,
     ID_java,
     symbol_table);
@@ -790,7 +795,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code.add(code_declt(return_code), loc);
 
   const refined_string_exprt string_expr =
-    make_nondet_string_expr(loc, function_name, symbol_table, code);
+    make_nondet_string_expr(loc, function_id, symbol_table, code);
 
   // args is { str.length, str.content, arguments... }
   exprt::operandst args;
@@ -798,10 +803,10 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   args.push_back(string_expr.content());
   args.insert(args.end(), arguments.begin(), arguments.end());
 
-  // return_code = <function_name>_data(args)
+  // return_code = <function_id>_data(args)
   code.add(
     code_assign_function_application(
-      return_code, function_name, args, symbol_table),
+      return_code, function_id, args, symbol_table),
     loc);
 
   return string_expr;
@@ -1070,7 +1075,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 }
 
 /// Generate the goto code for string initialization.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
@@ -1085,7 +1090,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 ///     cprover_string = {.=cprover_string_length, .=cprover_string_array};
 ///
 code_blockt java_string_library_preprocesst::make_init_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table,
@@ -1109,7 +1114,7 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
 
   // string_expr <- function(arg1)
   const refined_string_exprt string_expr =
-    string_expr_of_function(function_name, args, loc, symbol_table, code);
+    string_expr_of_function(function_id, args, loc, symbol_table, code);
 
   // arg_this <- string_expr
   code.add(
@@ -1122,14 +1127,14 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
 
 /// Call a cprover internal function, assign the result to object `this` and
 /// return it.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
 /// \return Code calling function with the given function name.
 code_blockt
 java_string_library_preprocesst::make_assign_and_return_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1140,22 +1145,21 @@ java_string_library_preprocesst::make_assign_and_return_function_from_call(
   PRECONDITION(!params[0].get_identifier().empty());
   code_blockt code;
   code.add(
-    make_assign_function_from_call(function_name, type, loc, symbol_table),
-    loc);
+    make_assign_function_from_call(function_id, type, loc, symbol_table), loc);
   const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
   code.add(code_returnt(arg_this), loc);
   return code;
 }
 
 /// Call a cprover internal function and assign the result to object `this`.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: the type of the function call
 /// \param loc: location in program
 /// \param symbol_table: the symbol table to populate
 /// \return Code assigning result of a call to the function with given function
 ///   name.
 code_blockt java_string_library_preprocesst::make_assign_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1163,7 +1167,7 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
   // This is similar to initialization function except we do not ignore
   // the first argument
   return make_init_function_from_call(
-    function_name, type, loc, symbol_table, false);
+    function_id, type, loc, symbol_table, false);
 }
 
 /// Adds to the code an assignment of the form
@@ -1574,16 +1578,16 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
 
 /// Provide code for a function that calls a function from the solver and simply
 /// returns it.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: type of the function
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// return function_name(args)
+/// return function_id(args)
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~
 code_blockt java_string_library_preprocesst::make_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1593,27 +1597,27 @@ code_blockt java_string_library_preprocesst::make_function_from_call(
     process_parameters(type.parameters(), loc, symbol_table, code);
   code.add(
     code_return_function_application(
-      function_name, args, type.return_type(), symbol_table),
+      function_id, args, type.return_type(), symbol_table),
     loc);
   return code;
 }
 
 /// Provide code for a function that calls a function from the solver and return
 /// the string_expr result as a Java string.
-/// \param function_name: name of the function to be called
+/// \param function_id: name of the function to be called
 /// \param type: type of the function
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
 /// \return Code corresponding to:
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-/// string_expr = function_name(args)
+/// string_expr = function_id(args)
 /// string = new String
 /// string = string_expr_to_string(string)
 /// return string
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 code_blockt
 java_string_library_preprocesst::make_string_returning_function_from_call(
-  const irep_idt &function_name,
+  const irep_idt &function_id,
   const java_method_typet &type,
   const source_locationt &loc,
   symbol_table_baset &symbol_table)
@@ -1627,11 +1631,11 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
-    string_expr_of_function(function_name, arguments, loc, symbol_table, code);
+    string_expr_of_function(function_id, arguments, loc, symbol_table, code);
 
   // Assign to string
   const exprt str = allocate_fresh_string(
-    type.return_type(), loc, function_name, symbol_table, code);
+    type.return_type(), loc, function_id, symbol_table, code);
   code.add(
     code_assign_string_expr_to_java_string(
       str, string_expr, symbol_table, true),
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index a825f2129f1..2068737d77a 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -193,6 +193,7 @@ class java_string_library_preprocesst:public messaget
     java_string_library_preprocesst &preprocess,
     const exprt &deref,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_tablet &symbol_table,
     code_blockt &init_code);
 
@@ -200,6 +201,7 @@ class java_string_library_preprocesst:public messaget
     const exprt &deref,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
+    const irep_idt &function_name,
     code_blockt &init_code);
 
   exprt::operandst process_operands(
diff --git a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index 283c81f0c37..11a316fc387 100644
--- a/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/jbmc/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -21,11 +21,12 @@ refined_string_exprt convert_exprt_to_string_exprt_unit_test(
   java_string_library_preprocesst &preprocess,
   const exprt &deref,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_tablet &symbol_table,
   code_blockt &init_code)
 {
   return preprocess.convert_exprt_to_string_exprt(
-    deref, loc, symbol_table, init_code);
+    deref, loc, symbol_table, function_id, init_code);
 }
 
 TEST_CASE("Convert exprt to string exprt")
@@ -33,6 +34,7 @@ TEST_CASE("Convert exprt to string exprt")
   GIVEN("A location, a string expression, and a symbol table")
   {
     source_locationt loc;
+    loc.set_function("function_name");
     symbol_tablet symbol_table;
     namespacet ns(symbol_table);
     code_blockt code;
@@ -45,9 +47,9 @@ TEST_CASE("Convert exprt to string exprt")
     {
       refined_string_exprt string_expr =
         convert_exprt_to_string_exprt_unit_test(
-          preprocess, expr, loc, symbol_table, code);
+          preprocess, expr, loc, "function_id", symbol_table, code);
 
-      THEN("The type of the returd expression is that of refined strings")
+      THEN("The type of the returned expression is that of refined strings")
       {
         REQUIRE(string_expr.id() == ID_struct);
         REQUIRE(is_refined_string_type(string_expr.type()));

From 5d13ed0d5dadb8870b027d8fed3980198390ca04 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 10:29:28 +0000
Subject: [PATCH 03/14] Add function_id parameter to decl_string_expr

This is in preparation for giving function_id as an argument to the
function creating fresh java symbols.
---
 .../java_string_library_preprocess.cpp            | 11 +++++++----
 .../java_string_library_preprocess.h              | 15 ++++++++-------
 2 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 54f5caae3c7..7f57d098fa8 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -306,7 +306,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 {
   PRECONDITION(implements_java_char_sequence_pointer(expr_to_process.type()));
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, init_code);
+    decl_string_expr(loc, function_id, symbol_table, init_code);
   code_assign_java_string_to_string_expr(
     string_expr, expr_to_process, loc, symbol_table, init_code);
   return string_expr;
@@ -496,11 +496,13 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
 /// Add declaration of a refined string expr whose content and length are
 /// fresh symbols.
 /// \param loc: source location
+/// \param function_id: name of the function in which the string is defined
 /// \param symbol_table: the symbol table
 /// \param [out] code: code block to which the declaration is added
 /// \return refined string expr with fresh content and length symbols
 refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -542,7 +544,8 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   code_blockt &code)
 {
   /// \todo refactor with initialize_nonddet_string_struct
-  const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
+  const refined_string_exprt str =
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
@@ -1671,7 +1674,7 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, code);
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   // Assign the argument to string_expr
   const java_method_typet::parametert &op = type.parameters()[0];
@@ -1718,7 +1721,7 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
-    decl_string_expr(loc, symbol_table, code);
+    decl_string_expr(loc, function_id, symbol_table, code);
 
   // Assign argument to a string_expr
   const java_method_typet::parameterst &params = type.parameters();
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 2068737d77a..470e6519c8b 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -234,6 +234,7 @@ class java_string_library_preprocesst:public messaget
 
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
@@ -251,13 +252,13 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   codet code_return_function_application(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const typet &type,
     symbol_table_baset &symbol_table);
 
   refined_string_exprt string_expr_of_function(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const exprt::operandst &arguments,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
@@ -290,32 +291,32 @@ class java_string_library_preprocesst:public messaget
     code_blockt &code);
 
   code_blockt make_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_init_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table,
     bool is_constructor = true);
 
   code_blockt make_assign_and_return_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_assign_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
   code_blockt make_string_returning_function_from_call(
-    const irep_idt &function_name,
+    const irep_idt &function_id,
     const java_method_typet &type,
     const source_locationt &loc,
     symbol_table_baset &symbol_table);

From 36c7b6c5369b977ae9b89e69028710466d66efb5 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 14:03:48 +0000
Subject: [PATCH 04/14] Add function_id parameter to process_operands

This is in preparation for adding the function_id to the function
generating fresh java symbols.
---
 .../java_string_library_preprocess.cpp         | 18 +++++++++++-------
 .../java_string_library_preprocess.h           |  2 ++
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 7f57d098fa8..577913e862b 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -265,6 +265,7 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 /// calls string_refine_preprocesst::process_operands with a list of parameters.
 /// \param params: a list of function parameters
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
@@ -272,13 +273,14 @@ symbol_exprt java_string_library_preprocesst::fresh_array(
 exprt::operandst java_string_library_preprocesst::process_parameters(
   const java_method_typet::parameterst &params,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
   exprt::operandst ops;
   for(const auto &p : params)
     ops.emplace_back(symbol_exprt(p.get_identifier(), p.type()));
-  return process_operands(ops, loc, symbol_table, init_code);
+  return process_operands(ops, loc, function_id, symbol_table, init_code);
 }
 
 /// Creates a string_exprt from the input exprt representing a char sequence
@@ -319,6 +321,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 /// for char array references.
 /// \param operands: a list of expressions
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
@@ -326,6 +329,7 @@ java_string_library_preprocesst::convert_exprt_to_string_exprt(
 exprt::operandst java_string_library_preprocesst::process_operands(
   const exprt::operandst &operands,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &init_code)
 {
@@ -335,7 +339,7 @@ exprt::operandst java_string_library_preprocesst::process_operands(
     if(implements_java_char_sequence_pointer(p.type()))
       ops.push_back(
         convert_exprt_to_string_exprt(
-          p, loc, symbol_table, loc.get_function(), init_code));
+          p, loc, symbol_table, function_id, init_code));
     else if(is_java_char_array_pointer_type(p.type()))
       ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
     else
@@ -1113,7 +1117,7 @@ code_blockt java_string_library_preprocesst::make_init_function_from_call(
 
   // Processing parameters
   const exprt::operandst args =
-    process_parameters(params, loc, symbol_table, code);
+    process_parameters(params, loc, function_id, symbol_table, code);
 
   // string_expr <- function(arg1)
   const refined_string_exprt string_expr =
@@ -1456,8 +1460,8 @@ code_blockt java_string_library_preprocesst::make_string_format_code(
 {
   PRECONDITION(type.parameters().size()==2);
   code_blockt code;
-  exprt::operandst args=process_parameters(
-    type.parameters(), loc, symbol_table, code);
+  exprt::operandst args =
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
   INVARIANT(args.size()==2, "String.format should have two arguments");
 
   // The argument can be:
@@ -1597,7 +1601,7 @@ code_blockt java_string_library_preprocesst::make_function_from_call(
 {
   code_blockt code;
   const exprt::operandst args =
-    process_parameters(type.parameters(), loc, symbol_table, code);
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
   code.add(
     code_return_function_application(
       function_id, args, type.return_type(), symbol_table),
@@ -1630,7 +1634,7 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
 
   // Calling the function
   const exprt::operandst arguments =
-    process_parameters(type.parameters(), loc, symbol_table, code);
+    process_parameters(type.parameters(), loc, function_id, symbol_table, code);
 
   // String expression that will hold the result
   const refined_string_exprt string_expr =
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 470e6519c8b..fe5b09e9ec2 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -185,6 +185,7 @@ class java_string_library_preprocesst:public messaget
   exprt::operandst process_parameters(
     const java_method_typet::parameterst &params,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
@@ -207,6 +208,7 @@ class java_string_library_preprocesst:public messaget
   exprt::operandst process_operands(
     const exprt::operandst &operands,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 

From 276e5346af45b7ee1a965fd5056f446dab452331 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 7 Feb 2019 11:29:01 +0000
Subject: [PATCH 05/14] Add function_id parameter to replace_char_array

This is in preparation for giving the function name to the function
generating fresh java symbols.
---
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 5 ++++-
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 577913e862b..8c2fc50169b 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -341,7 +341,8 @@ exprt::operandst java_string_library_preprocesst::process_operands(
         convert_exprt_to_string_exprt(
           p, loc, symbol_table, function_id, init_code));
     else if(is_java_char_array_pointer_type(p.type()))
-      ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
+      ops.push_back(
+        replace_char_array(p, loc, function_id, symbol_table, init_code));
     else
       ops.push_back(p);
   }
@@ -447,12 +448,14 @@ static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
 /// array.
 /// \param array_pointer: an expression of type char array pointer
 /// \param loc: location in the source
+/// \param function_id: name of the function in which the string is defined
 /// \param symbol_table: symbol table
 /// \param code: code block, in which some assignments will be added
 /// \return a string expression
 refined_string_exprt java_string_library_preprocesst::replace_char_array(
   const exprt &array_pointer,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index fe5b09e9ec2..24084792c42 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -221,6 +221,7 @@ class java_string_library_preprocesst:public messaget
   refined_string_exprt replace_char_array(
     const exprt &array_pointer,
     const source_locationt &loc,
+    const irep_idt &function_name,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 

From 2189e409ca5ed143a7d2ff5afd7abadfc6878f52 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 13:07:14 +0000
Subject: [PATCH 06/14] Add function_id parameter to
 add_pointer_to_array_association

This is in preparation for giving the function name to the function
generating fresh java symbols.
---
 jbmc/src/java_bytecode/java_object_factory.cpp            | 2 +-
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 6 ++++--
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 9f9a52efec7..98f1eb6f20d 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -476,7 +476,7 @@ void initialize_nondet_string_fields(
     index_exprt(data_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
-    array_pointer, data_expr, symbol_table, loc, code);
+    array_pointer, data_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
     data_expr, length_expr, symbol_table, loc, code);
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 8c2fc50169b..8f90a4e5446 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -478,7 +478,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
 
   add_pointer_to_array_association(
-    string_expr.content(), inf_array, symbol_table, loc, code);
+    string_expr.content(), inf_array, symbol_table, loc, function_id, code);
 
   return string_expr;
 }
@@ -564,7 +564,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
 
   add_pointer_to_array_association(
-    array_pointer, nondet_array_expr, symbol_table, loc, code);
+    array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
     nondet_array_expr, str.length(), symbol_table, loc, code);
@@ -677,12 +677,14 @@ exprt make_nondet_infinite_char_array(
 /// \param array: a character array expression
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: name of the function in which the code will be added
 /// \param [out] code: code block to which declaration and calls get added
 void add_pointer_to_array_association(
   const exprt &pointer,
   const exprt &array,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   PRECONDITION(array.type().id() == ID_array);
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 24084792c42..2a80227dbdf 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -354,6 +354,7 @@ void add_pointer_to_array_association(
   const exprt &array,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 void add_array_to_length_association(

From 8c15acdd92f9e6868ca270ba5678d987974b5fdc Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 13:11:43 +0000
Subject: [PATCH 07/14] Add function_id parameter to
 add_array_to_length_association

This is in preparation to giving the function_id to the function
generating fresh java symbols.
---
 jbmc/src/java_bytecode/java_object_factory.cpp            | 2 +-
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 4 +++-
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 98f1eb6f20d..862c1ff8e73 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -479,7 +479,7 @@ void initialize_nondet_string_fields(
     array_pointer, data_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
-    data_expr, length_expr, symbol_table, loc, code);
+    data_expr, length_expr, symbol_table, loc, function_id, code);
 
   struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
 
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 8f90a4e5446..418f164eb76 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -567,7 +567,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
     array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
 
   add_array_to_length_association(
-    nondet_array_expr, str.length(), symbol_table, loc, code);
+    nondet_array_expr, str.length(), symbol_table, loc, function_id, code);
 
   code.add(code_assignt(str.content(), array_pointer), loc);
 
@@ -713,12 +713,14 @@ void add_pointer_to_array_association(
 /// \param length: integer expression
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: name of the function in which the code will be added
 /// \param [out] code: code block to which declaration and calls get added
 void add_array_to_length_association(
   const exprt &array,
   const exprt &length,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   const symbolt &return_sym = get_fresh_aux_symbol(
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 2a80227dbdf..3b48c2e4af8 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -362,6 +362,7 @@ void add_array_to_length_association(
   const exprt &length,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 void add_character_set_constraint(

From 0180b8bc579b63767bf5a66d56e1cff8a5100781 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 8 Feb 2019 10:12:25 +0000
Subject: [PATCH 08/14] Delete unused function fresh_array

This function is not used, there is no point in keeping it.
---
 .../java_string_library_preprocess.cpp        | 21 -------------------
 .../java_string_library_preprocess.h          |  5 -----
 2 files changed, 26 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 418f164eb76..cbf4b7ea7a2 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -241,27 +241,6 @@ void java_string_library_preprocesst::add_string_type(
   string_symbol->mode = ID_java;
 }
 
-/// add a symbol in the table with static lifetime and name containing
-/// `cprover_string_array` and given type
-/// \param type: an array type
-/// \param location: a location in the program
-/// \param symbol_table: symbol table
-symbol_exprt java_string_library_preprocesst::fresh_array(
-  const typet &type,
-  const source_locationt &location,
-  symbol_tablet &symbol_table)
-{
-  symbolt array_symbol=get_fresh_aux_symbol(
-    type,
-    "cprover_string_array",
-    "cprover_string_array",
-    location,
-    ID_java,
-    symbol_table);
-  array_symbol.is_static_lifetime=true;
-  return array_symbol.symbol_expr();
-}
-
 /// calls string_refine_preprocesst::process_operands with a list of parameters.
 /// \param params: a list of function parameters
 /// \param loc: location in the source
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 3b48c2e4af8..b6f0bcd253f 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -230,11 +230,6 @@ class java_string_library_preprocesst:public messaget
     const source_locationt &loc,
     symbol_table_baset &symbol_table);
 
-  symbol_exprt fresh_array(
-    const typet &type,
-    const source_locationt &loc,
-    symbol_tablet &symbol_table);
-
   refined_string_exprt decl_string_expr(
     const source_locationt &loc,
     const irep_idt &function_id,

From afb691d31d2131906cb1e83a8aaf117270bf3e6f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 8 Feb 2019 12:22:13 +0000
Subject: [PATCH 09/14] Delete unused function process_operands

This is not used
---
 .../java_string_library_preprocess.cpp        | 36 -------------------
 .../java_string_library_preprocess.h          |  6 ----
 2 files changed, 42 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index cbf4b7ea7a2..4d31c3bb984 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -328,42 +328,6 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   return ops;
 }
 
-/// Converts the operands of the equals function to string expressions and
-/// outputs these conversions. As a side effect of the conversions it adds some
-/// code to init_code.
-/// \param operands: a list of expressions
-/// \param loc: location in the source
-/// \param symbol_table: symbol table
-/// \param init_code: code block, in which declaration of some arguments may be
-///   added
-/// \return a list of expressions
-exprt::operandst
-java_string_library_preprocesst::process_equals_function_operands(
-  const exprt::operandst &operands,
-  const source_locationt &loc,
-  symbol_table_baset &symbol_table,
-  code_blockt &init_code)
-{
-  PRECONDITION(operands.size()==2);
-  exprt::operandst ops;
-  const exprt &op0=operands[0];
-  const exprt &op1 = operands[1];
-  PRECONDITION(implements_java_char_sequence_pointer(op0.type()));
-
-  ops.push_back(
-    convert_exprt_to_string_exprt(
-      op0, loc, symbol_table, loc.get_function(), init_code));
-
-  // TODO: Manage the case where we have a non-String Object (this should
-  // probably be handled upstream. At any rate, the following code should be
-  // protected with assertions on the type of op1.
-  const typecast_exprt tcast(op1, to_pointer_type(op0.type()));
-  ops.push_back(
-    convert_exprt_to_string_exprt(
-      tcast, loc, symbol_table, loc.get_function(), init_code));
-  return ops;
-}
-
 /// Finds the type of the data component
 /// \param type: a type containing a "data" component
 /// \param symbol_table: symbol table
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index b6f0bcd253f..f135a22a937 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -212,12 +212,6 @@ class java_string_library_preprocesst:public messaget
     symbol_table_baset &symbol_table,
     code_blockt &init_code);
 
-  exprt::operandst process_equals_function_operands(
-    const exprt::operandst &operands,
-    const source_locationt &loc,
-    symbol_table_baset &symbol_table,
-    code_blockt &init_code);
-
   refined_string_exprt replace_char_array(
     const exprt &array_pointer,
     const source_locationt &loc,

From d3f768c1385193bbfe5a39348e26642b3149f450 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Nov 2018 13:36:47 +0000
Subject: [PATCH 10/14] Add function_id parameter to fresh_string

This is in preparation to giving the function_id to the function
generating fresh java symbols.
---
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 4 +++-
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 4d31c3bb984..be8f82a955c 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -430,11 +430,13 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
 /// given type
 /// \param type: a type for refined strings
 /// \param loc: a location in the program
+/// \param function_id: name of the function in which the code will be added
 /// \param symbol_table: symbol table
 /// \return a new symbol
 symbol_exprt java_string_library_preprocesst::fresh_string(
   const typet &type,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
   symbolt string_symbol=get_fresh_aux_symbol(
@@ -531,7 +533,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  const exprt str = fresh_string(type, loc, symbol_table);
+  const exprt str = fresh_string(type, loc, function_id, symbol_table);
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index f135a22a937..03d2ac6b451 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -222,6 +222,7 @@ class java_string_library_preprocesst:public messaget
   symbol_exprt fresh_string(
     const typet &type,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table);
 
   refined_string_exprt decl_string_expr(

From 06f89d9a72afff8e8d799753edfa99c7ceba62a0 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 8 Feb 2019 10:20:37 +0000
Subject: [PATCH 11/14] Add function_id parameter to
 add_character_set_constraint

This is in preparation for using a new fresh_java_symbol function which
takes a function_id as parameter.
---
 jbmc/src/java_bytecode/java_object_factory.cpp            | 2 +-
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 2 ++
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 3 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 862c1ff8e73..82dc500f49b 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -487,7 +487,7 @@ void initialize_nondet_string_fields(
   if(printable)
   {
     add_character_set_constraint(
-      array_pointer, length_expr, " -~", symbol_table, loc, code);
+      array_pointer, length_expr, " -~", symbol_table, loc, function_id, code);
   }
 }
 
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index be8f82a955c..d8fab5fb378 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -695,6 +695,7 @@ void add_array_to_length_association(
 ///   lower case ascii letters.
 /// \param symbol_table: the symbol table
 /// \param loc: source location
+/// \param function_id: the name of the function
 /// \param [out] code: code block to which declaration and calls get added
 void add_character_set_constraint(
   const exprt &pointer,
@@ -702,6 +703,7 @@ void add_character_set_constraint(
   const irep_idt &char_set,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index 03d2ac6b451..f864321f086 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -361,6 +361,7 @@ void add_character_set_constraint(
   const irep_idt &char_set,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &code);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H

From b4e146abb8a4470e3af8094f2c3d5d2fa3562c16 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 8 Feb 2019 10:23:05 +0000
Subject: [PATCH 12/14] Add function_id parameter to
 get_primitive_value_of_object

This is in preparation to giving the function_id to the function
generating fresh java symbols.
---
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 4 +++-
 jbmc/src/java_bytecode/java_string_library_preprocess.h   | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index d8fab5fb378..c43aeef1421 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1145,6 +1145,7 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
 ///   one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int,
 ///   ID_long, ID_float, ID_double, ID_void
 /// \param loc: a location in the source
+/// \param function_id: the name of the function
 /// \param symbol_table: the symbol table
 /// \param code: code block to which we are adding some assignments
 /// \return An expression containing a symbol `tmp_type_name` where `type_name`
@@ -1155,6 +1156,7 @@ java_string_library_preprocesst::get_primitive_value_of_object(
   const exprt &object,
   irep_idt type_name,
   const source_locationt &loc,
+  const irep_idt &function_id,
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
@@ -1379,7 +1381,7 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
     else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
     {
       const auto value = get_primitive_value_of_object(
-        arg_i, name, loc, symbol_table, code_not_null);
+        arg_i, name, loc, function_id, symbol_table, code_not_null);
       if(value.has_value())
         code_not_null.add(code_assignt(field_expr, *value), loc);
       else
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index f864321f086..12d4a4f8774 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -327,6 +327,7 @@ class java_string_library_preprocesst:public messaget
     const exprt &object,
     irep_idt type_name,
     const source_locationt &loc,
+    const irep_idt &function_id,
     symbol_table_baset &symbol_table,
     code_blockt &code);
 

From 3edbc74aa66cfd3d4dc61466867ac0a3c73cfe98 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 9 Aug 2018 08:35:15 +0100
Subject: [PATCH 13/14] Add and use fresh_java_symbol function

This prevents forgetting that the basename of the symbol should be the
function identifier.
---
 .../src/java_bytecode/convert_java_nondet.cpp | 11 +--
 ...a_bytecode_concurrency_instrumentation.cpp |  7 +-
 .../java_bytecode_instrument.cpp              | 11 +--
 jbmc/src/java_bytecode/java_entry_point.cpp   |  5 +-
 .../src/java_bytecode/java_object_factory.cpp | 18 ++---
 .../java_string_library_preprocess.cpp        | 79 ++++++-------------
 jbmc/src/java_bytecode/java_utils.cpp         | 21 +++++
 jbmc/src/java_bytecode/java_utils.h           |  7 ++
 jbmc/src/java_bytecode/remove_instanceof.cpp  | 16 ++--
 jbmc/src/java_bytecode/remove_java_new.cpp    | 31 +++-----
 .../java_bytecode/simple_method_stubbing.cpp  | 12 ++-
 11 files changed, 93 insertions(+), 125 deletions(-)

diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
index 427122e1992..a5d4b8fa19f 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -15,12 +15,12 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include <util/fresh_symbol.h>
 #include <util/irep_ids.h>
 
 #include <memory>
 
 #include "java_object_factory.h" // gen_nondet_init
+#include "java_utils.h"
 
 /// Returns true if `expr` is a nondet pointer that isn't a function pointer or
 /// a void* pointer as these can be meaningfully non-det initialized.
@@ -116,13 +116,8 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
     //   target2: instruction containing op, with op replaced by aux_symbol
     //            dead aux_symbol
 
-    symbolt &aux_symbol = get_fresh_aux_symbol(
-      op.type(),
-      id2string(function_identifier),
-      "nondet_tmp",
-      source_loc,
-      ID_java,
-      symbol_table);
+    symbolt &aux_symbol = fresh_java_symbol(
+      op.type(), "nondet_tmp", source_loc, function_identifier, symbol_table);
 
     const symbol_exprt aux_symbol_expr = aux_symbol.symbol_expr();
     op = aux_symbol_expr;
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index eb1a43696f8..76417570344 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -9,12 +9,12 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com
 #include "java_bytecode_concurrency_instrumentation.h"
 #include "expr2java.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 #include <util/expr_iterator.h>
 #include <util/namespace.h>
 #include <util/cprover_prefix.h>
 #include <util/std_types.h>
-#include <util/fresh_symbol.h>
 #include <util/arith_tools.h>
 
 // Disable linter to allow an std::string constant.
@@ -229,12 +229,11 @@ static void instrument_synchronized_code(
   code_pop_catcht catch_pop;
 
   // Create the finally block with the same label targeted in the catch-push
-  const symbolt &tmp_symbol = get_fresh_aux_symbol(
+  const symbolt &tmp_symbol = fresh_java_symbol(
     java_reference_type(struct_tag_typet("java::java.lang.Throwable")),
-    id2string(symbol.name),
     "caught-synchronized-exception",
     code.source_location(),
-    ID_java,
+    id2string(symbol.name),
     symbol_table);
   symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type);
   catch_var.set(ID_C_base_name, tmp_symbol.base_name);
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
index 3b11e293fdf..4ae7ae42741 100644
--- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -11,7 +11,6 @@ Date:   June 2017
 #include "java_bytecode_instrument.h"
 
 #include <util/arith_tools.h>
-#include <util/fresh_symbol.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/c_types.h>
@@ -112,14 +111,8 @@ code_ifthenelset java_bytecode_instrumentt::throw_exception(
 
   // Allocate and throw an instance of the exception class:
 
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      exc_ptr_type,
-      "new_exception",
-      "new_exception",
-      original_loc,
-      ID_java,
-      symbol_table);
+  symbolt &new_symbol = fresh_java_symbol(
+    exc_ptr_type, "new_exception", original_loc, "new_exception", symbol_table);
 
   side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 39a834cc3da..30284035635 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -375,12 +375,11 @@ exprt::operandst java_build_arguments(
       // method(..., param, ...)
       //
 
-      const symbolt result_symbol = get_fresh_aux_symbol(
+      const symbolt result_symbol = fresh_java_symbol(
         p.type(),
-        id2string(function.name),
         "nondet_parameter_" + std::to_string(param_number),
         function.location,
-        ID_java,
+        function.name,
         symbol_table);
       main_arguments[param_number] = result_symbol.symbol_expr();
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 82dc500f49b..a8d7e204ec5 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_object_factory.h"
 
 #include <util/expr_initializer.h>
-#include <util/fresh_symbol.h>
 #include <util/nondet_bool.h>
 #include <util/nondet.h>
 #include <util/pointer_offset_size.h>
@@ -20,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "generic_parameter_specialization_map_keys.h"
 #include "java_root_class.h"
 #include "java_string_literals.h"
+#include "java_utils.h"
 
 class java_object_factoryt
 {
@@ -442,13 +442,8 @@ void initialize_nondet_string_fields(
 
   /// \todo Refactor with make_nondet_string_expr
   // length_expr = nondet(int);
-  const symbolt length_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    id2string(function_id),
-    "tmp_object_factory",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt length_sym = fresh_java_symbol(
+    java_int_type(), "tmp_object_factory", loc, function_id, symbol_table);
   const symbol_exprt length_expr = length_sym.symbol_expr();
   const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
   code.add(code_declt(length_expr));
@@ -745,12 +740,11 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   size_t depth,
   const source_locationt &location)
 {
-  symbolt new_symbol = get_fresh_aux_symbol(
+  symbolt new_symbol = fresh_java_symbol(
     replacement_pointer,
-    id2string(object_factory_parameters.function_id),
     "tmp_object_factory",
-    loc,
-    ID_java,
+    location,
+    object_factory_parameters.function_id,
     symbol_table);
 
   // Generate a new object into this new symbol
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index c43aeef1421..2643f6f1376 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -407,8 +407,8 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     checked_dereference(array_pointer, array_pointer.type().subtype());
   // array_data is array_pointer-> data
   const exprt array_data = get_data(array, symbol_table);
-  const symbolt &sym_char_array = get_fresh_aux_symbol(
-    array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
+  const symbolt &sym_char_array = fresh_java_symbol(
+    array_data.type(), "char_array", loc, function_id, symbol_table);
   const symbol_exprt char_array = sym_char_array.symbol_expr();
   // char_array = array_pointer->data
   code.add(code_assignt(char_array, array_data), loc);
@@ -439,8 +439,8 @@ symbol_exprt java_string_library_preprocesst::fresh_string(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table)
 {
-  symbolt string_symbol=get_fresh_aux_symbol(
-    type, "cprover_string", "cprover_string", loc, ID_java, symbol_table);
+  symbolt string_symbol =
+    fresh_java_symbol(type, "cprover_string", loc, function_id, symbol_table);
   string_symbol.is_static_lifetime=true;
   return string_symbol.symbol_expr();
 }
@@ -458,22 +458,12 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
-  const symbolt &sym_length = get_fresh_aux_symbol(
-    index_type,
-    "cprover_string_length",
-    "cprover_string_length",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &sym_length = fresh_java_symbol(
+    index_type, "cprover_string_length", loc, function_id, symbol_table);
   const symbol_exprt length_field = sym_length.symbol_expr();
   const pointer_typet array_type = pointer_type(java_char_type());
-  const symbolt &sym_content = get_fresh_aux_symbol(
-    array_type,
-    "cprover_string_content",
-    "cprover_string_content",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &sym_content = fresh_java_symbol(
+    array_type, "cprover_string_content", loc, function_id, symbol_table);
   const symbol_exprt content_field = sym_content.symbol_expr();
   code.add(code_declt(content_field), loc);
   const refined_string_exprt str{
@@ -599,12 +589,11 @@ exprt make_nondet_infinite_char_array(
 {
   const array_typet array_type(
     java_char_type(), infinity_exprt(java_int_type()));
-  const symbolt data_sym = get_fresh_aux_symbol(
+  const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
-    id2string(function_id),
     "nondet_infinite_array_pointer",
     loc,
-    ID_java,
+    function_id,
     symbol_table);
 
   const symbol_exprt data_pointer = data_sym.symbol_expr();
@@ -634,13 +623,8 @@ void add_pointer_to_array_association(
 {
   PRECONDITION(array.type().id() == ID_array);
   PRECONDITION(pointer.type().id() == ID_pointer);
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -668,13 +652,8 @@ void add_array_to_length_association(
   const irep_idt &function_id,
   code_blockt &code)
 {
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(),
-    "return_array",
-    "return_array",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "return_array", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   code.add(
@@ -707,8 +686,8 @@ void add_character_set_constraint(
   code_blockt &code)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
-  const symbolt &return_sym = get_fresh_aux_symbol(
-    java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
+  const symbolt &return_sym = fresh_java_symbol(
+    java_int_type(), "cnstr_added", loc, function_id, symbol_table);
   const auto return_expr = return_sym.symbol_expr();
   code.add(code_declt(return_expr), loc);
   const constant_exprt char_set_expr(char_set, string_typet());
@@ -745,12 +724,11 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
   code_blockt &code)
 {
   // int return_code;
-  const symbolt &return_code_sym = get_fresh_aux_symbol(
+  const symbolt return_code_sym = fresh_java_symbol(
     java_int_type(),
     std::string("return_code_") + function_id.c_str(),
-    std::string("return_code_") + function_id.c_str(),
     loc,
-    ID_java,
+    function_id,
     symbol_table);
   const auto return_code = return_code_sym.symbol_expr();
   code.add(code_declt(return_code), loc);
@@ -1212,8 +1190,8 @@ java_string_library_preprocesst::get_primitive_value_of_object(
 
   // declare tmp_type_name to hold the value
   const std::string aux_name = "tmp_" + id2string(type_name);
-  const symbolt &symbol = get_fresh_aux_symbol(
-    value_type, aux_name, aux_name, loc, ID_java, symbol_table);
+  const symbolt &symbol =
+    fresh_java_symbol(value_type, aux_name, loc, function_id, symbol_table);
   const auto value = symbol.symbol_expr();
 
   // Check that the type of the object is in the symbol table,
@@ -1318,8 +1296,8 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
     if(name!="string_expr")
     {
       std::string tmp_name="tmp_"+id2string(name);
-      const symbolt &field_symbol = get_fresh_aux_symbol(
-        type, id2string(function_id), tmp_name, loc, ID_java, symbol_table);
+      const symbolt &field_symbol =
+        fresh_java_symbol(type, tmp_name, loc, function_id, symbol_table);
       auto field_symbol_expr = field_symbol.symbol_expr();
       field_expr = field_symbol_expr;
       code.add(code_declt(field_symbol_expr), loc);
@@ -1334,13 +1312,8 @@ struct_exprt java_string_library_preprocesst::make_argument_for_format(
 
   // arg_i = argv[index]
   const exprt obj = get_object_at_index(argv, index);
-  const symbolt &object_symbol = get_fresh_aux_symbol(
-    obj.type(),
-    id2string(function_id),
-    "tmp_format_obj",
-    loc,
-    ID_java,
-    symbol_table);
+  const symbolt &object_symbol = fresh_java_symbol(
+    obj.type(), "tmp_format_obj", loc, function_id, symbol_table);
   const symbol_exprt arg_i = object_symbol.symbol_expr();
 
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
@@ -1485,8 +1458,8 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code(
   // > Class class1;
   const pointer_typet class_type =
     java_reference_type(symbol_table.lookup_ref("java::java.lang.Class").type);
-  const symbolt &class1_sym = get_fresh_aux_symbol(
-    class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
+  const symbolt &class1_sym = fresh_java_symbol(
+    class_type, "class_symbol", loc, function_id, symbol_table);
   const symbol_exprt class1 = class1_sym.symbol_expr();
   code.add(code_declt(class1), loc);
 
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 86b8d1043bd..234c136d3fd 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/jbmc/src/java_bytecode/java_utils.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "java_root_class.h"
 
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/message.h>
@@ -433,3 +434,23 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
   "endThread",
   "getCurrentThreadID"
 };
+
+/// \param type: type of new symbol
+/// \param basename_prefix: new symbol will be named
+///   function_name::basename_prefix$num
+/// \param source_location: new symbol source loc
+/// \param function_name: name of the function in which the symbol is defined
+/// \param symbol_table: table to add the new symbol to
+/// \return fresh-named symbol with the requested name pattern
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table)
+{
+  PRECONDITION(!function_name.empty());
+  const std::string name_prefix = id2string(function_name);
+  return get_fresh_aux_symbol(
+    type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
+}
diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h
index 128d6268671..70d1b30d504 100644
--- a/jbmc/src/java_bytecode/java_utils.h
+++ b/jbmc/src/java_bytecode/java_utils.h
@@ -109,4 +109,11 @@ bool is_non_null_library_global(const irep_idt &);
 
 extern const std::unordered_set<std::string> cprover_methods_to_ignore;
 
+symbolt &fresh_java_symbol(
+  const typet &type,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &function_name,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
index 24a0260953a..cfcb04fed7d 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.cpp
+++ b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -10,12 +10,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// Remove Instance-of Operators
 
 #include "remove_instanceof.h"
+#include "java_utils.h"
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
-#include <util/fresh_symbol.h>
 #include <java_bytecode/java_types.h>
 
 #include <sstream>
@@ -116,20 +116,18 @@ bool remove_instanceoft::lower_instanceof(
   auto jlo = to_struct_tag_type(java_lang_object_type().subtype());
   exprt object_clsid = get_class_identifier_field(check_ptr, jlo, ns);
 
-  symbolt &clsid_tmp_sym = get_fresh_aux_symbol(
+  symbolt &clsid_tmp_sym = fresh_java_symbol(
     object_clsid.type(),
-    id2string(function_identifier),
     "class_identifier_tmp",
-    source_locationt(),
-    ID_java,
+    this_inst->source_location,
+    function_identifier,
     symbol_table);
 
-  symbolt &instanceof_result_sym = get_fresh_aux_symbol(
+  symbolt &instanceof_result_sym = fresh_java_symbol(
     bool_typet(),
-    id2string(function_identifier),
     "instanceof_result_tmp",
-    source_locationt(),
-    ID_java,
+    this_inst->source_location,
+    function_identifier,
     symbol_table);
 
   // Create
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
index 6750ac30fd6..6825005ca5f 100644
--- a/jbmc/src/java_bytecode/remove_java_new.cpp
+++ b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -14,11 +14,11 @@ Author: Peter Schrammel
 #include <goto-programs/class_identifier.h>
 #include <goto-programs/goto_convert.h>
 
+#include "java_utils.h"
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_cast.h>
 #include <util/expr_initializer.h>
-#include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
 
@@ -212,12 +212,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   // Must directly assign the new array to a temporary
   // because goto-symex will notice `x=side_effect_exprt` but not
   // `x=typecast_exprt(side_effect_exprt(...))`
-  symbol_exprt new_array_data_symbol = get_fresh_aux_symbol(
+  symbol_exprt new_array_data_symbol = fresh_java_symbol(
                                          data_java_new_expr.type(),
-                                         id2string(function_identifier),
                                          "tmp_new_data_array",
                                          location,
-                                         ID_java,
+                                         function_identifier,
                                          symbol_table)
                                          .symbol_expr();
   code_declt array_decl(new_array_data_symbol);
@@ -260,14 +259,10 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
 
     goto_programt tmp;
 
-    symbol_exprt tmp_i = get_fresh_aux_symbol(
-                           length.type(),
-                           id2string(function_identifier),
-                           "tmp_index",
-                           location,
-                           ID_java,
-                           symbol_table)
-                           .symbol_expr();
+    symbol_exprt tmp_i =
+      fresh_java_symbol(
+        length.type(), "tmp_index", location, function_identifier, symbol_table)
+        .symbol_expr();
     code_declt decl(tmp_i);
     decl.add_source_location() = location;
     goto_programt::targett t_decl = tmp.insert_before(tmp.instructions.begin());
@@ -292,14 +287,10 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
       plus_exprt(data, tmp_i), data.type().subtype());
 
     code_blockt for_body;
-    symbol_exprt init_sym = get_fresh_aux_symbol(
-                              sub_type,
-                              id2string(function_identifier),
-                              "subarray_init",
-                              location,
-                              ID_java,
-                              symbol_table)
-                              .symbol_expr();
+    symbol_exprt init_sym =
+      fresh_java_symbol(
+        sub_type, "subarray_init", location, function_identifier, symbol_table)
+        .symbol_expr();
     code_declt init_decl(init_sym);
     init_decl.add_source_location() = location;
     for_body.add(std::move(init_decl));
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 4c75878c20c..378f9c14da7 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -14,7 +14,7 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_object_factory.h>
 #include <java_bytecode/java_pointer_casts.h>
 
-#include <util/fresh_symbol.h>
+#include "java_utils.h"
 #include <util/invariant_utils.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
@@ -161,12 +161,11 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
   {
     const auto &this_argument = required_type.parameters()[0];
     const typet &this_type = this_argument.type();
-    symbolt &init_symbol = get_fresh_aux_symbol(
+    symbolt &init_symbol = fresh_java_symbol(
       this_type,
-      id2string(symbol.name),
       "to_construct",
       synthesized_source_location,
-      ID_java,
+      symbol.name,
       symbol_table);
     const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
     code_assignt get_argument(
@@ -189,12 +188,11 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
     const typet &required_return_type = required_type.return_type();
     if(required_return_type != java_void_type())
     {
-      symbolt &to_return_symbol = get_fresh_aux_symbol(
+      symbolt &to_return_symbol = fresh_java_symbol(
         required_return_type,
-        id2string(symbol.name),
         "to_return",
         synthesized_source_location,
-        ID_java,
+        symbol.name,
         symbol_table);
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)

From e81e174e8b9255f29a1f2f63b58b8295fdbbfd89 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 6 Feb 2019 11:42:48 +0000
Subject: [PATCH 14/14] Apply clang-format suggestions

No functional changes.
---
 jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 2643f6f1376..edf38dd76b0 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -316,9 +316,8 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   for(const auto &p : operands)
   {
     if(implements_java_char_sequence_pointer(p.type()))
-      ops.push_back(
-        convert_exprt_to_string_exprt(
-          p, loc, symbol_table, function_id, init_code));
+      ops.push_back(convert_exprt_to_string_exprt(
+        p, loc, symbol_table, function_id, init_code));
     else if(is_java_char_array_pointer_type(p.type()))
       ops.push_back(
         replace_char_array(p, loc, function_id, symbol_table, init_code));