From df36fecdef239ef7ede60f4873d28e199ca30dc9 Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 23 Mar 2017 15:05:27 +0000 Subject: [PATCH] const refs and clean up Corrections on PR 675 requested by Peter Schrammel --- src/goto-programs/string_refine_preprocess.cpp | 10 ++++++---- .../refinement/string_constraint_generator_main.cpp | 12 ++++++++++++ src/solvers/refinement/string_refinement.h | 3 --- 3 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/goto-programs/string_refine_preprocess.cpp b/src/goto-programs/string_refine_preprocess.cpp index 7243f66049a..8b491bab0ab 100644 --- a/src/goto-programs/string_refine_preprocess.cpp +++ b/src/goto-programs/string_refine_preprocess.cpp @@ -809,11 +809,13 @@ void string_refine_preprocesst::make_string_function_side_effect( const irep_idt &function_name, const std::string &signature) { + // Cannot use const & here code_function_callt function_call=to_code_function_call(target->code); source_locationt loc=function_call.source_location(); std::list 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 +903,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 +987,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); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index f8dedaab9a7..e4292da542b 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/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) { diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 252146f4620..0a62a6abe7d 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/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