Corrections on PR 675

Remarks by Peter Schrammel

Author: Joel Allred

src/goto-programs/string_refine_preprocess.cpp

@@ -809,11 +809,14 @@ void string_refine_preprocesst::make_string_function_side_effect(
   const irep_idt &function_name,
   const std::string &signature)
 {
+  // TODO: Here we create a copy of the code_function_cally. We would prefer
+  // accessing it by reference, but this creates problems.
   code_function_callt function_call=to_code_function_call(target->code);
   source_locationt loc=function_call.source_location();
   std::list<code_assignt> assignments;
-  exprt lhs=function_call.lhs();
-  exprt s=function_call.arguments()[0];
+  const exprt &lhs=function_call.lhs();
+  assert(!function_call.arguments().empty());
+  const exprt &s=function_call.arguments()[0];
   code_typet function_type=to_code_type(function_call.type());
 
   function_type.return_type()=s.type();
@@ -901,7 +904,7 @@ void string_refine_preprocesst::make_to_char_array_function(
   const code_function_callt &function_call=to_code_function_call(target->code);
   source_locationt location=function_call.source_location();
 
-  assert(function_call.arguments().size()>=1);
+  assert(!function_call.arguments().empty());
   const exprt &string_argument=function_call.arguments()[0];
   assert(is_java_string_pointer_type(string_argument.type()));
 
@@ -985,7 +988,7 @@ exprt::operandst string_refine_preprocesst::process_arguments(
         arg=typecast_exprt(arg, jls_ptr);
     }
     arg=make_cprover_string_assign(goto_program, target, arg, location);
-    typet type=ns.follow(arg.type());
+    const typet &type=ns.follow(arg.type());
     if(is_java_char_array_pointer_type(type))
     {
       arg=make_cprover_char_array_assign(goto_program, target, arg, location);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -208,6 +208,18 @@ string_exprt string_constraint_generatort::get_string_expr(const exprt &expr)
   }
 }
 
+/*******************************************************************\
+
+Function: string_constraint_generatort::convert_java_string_to_string_exprt
+
+  Inputs: a java string
+
+ Outputs: a string expression
+
+ Purpose: create a new string_exprt as a conversion of a java string
+
+\*******************************************************************/
+
 string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
     const exprt &jls)
 {

src/solvers/refinement/string_refinement.h

@@ -63,9 +63,6 @@ class string_refinementt: public bv_refinementt
 
   unsigned initial_loop_bound;
 
-  // Is the current model correct
-  bool concrete_model;
-
   string_constraint_generatort generator;
 
   // Simple constraints that have been given to the solver