From 03123a99413a928bcb611a610d63ce6490892c82 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 20:29:29 +0000 Subject: [PATCH 1/9] taint_analysis: make last argument optional We previously passed in empty strings. Make explicit that the argument is not required. --- jbmc/src/janalyzer/janalyzer_parse_options.cpp | 2 +- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- src/goto-analyzer/taint_analysis.h | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 5e661a8a38b..682cbbc5991 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -405,7 +405,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-taint")) { - taint_analysis(goto_model, taint_file, ui_message_handler, true, ""); + taint_analysis(goto_model, taint_file, ui_message_handler, true); return CPROVER_EXIT_SUCCESS; } else diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 8b38b9188e6..962cbd39dbb 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -442,7 +442,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) if(cmdline.isset("show-taint")) { - taint_analysis(goto_model, taint_file, ui_message_handler, true, ""); + taint_analysis(goto_model, taint_file, ui_message_handler, true); return CPROVER_EXIT_SUCCESS; } else diff --git a/src/goto-analyzer/taint_analysis.h b/src/goto-analyzer/taint_analysis.h index f9b73d2640e..38390ee646e 100644 --- a/src/goto-analyzer/taint_analysis.h +++ b/src/goto-analyzer/taint_analysis.h @@ -22,6 +22,6 @@ bool taint_analysis( const std::string &taint_file_name, message_handlert &, bool show_full, - const std::string &json_file_name); + const std::string &json_output_file_name = ""); #endif // CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H From ec56872cdc0b9a68c847ee80799f0cdc61995d1f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 20:30:51 +0000 Subject: [PATCH 2/9] Use s.empty() instead of s == "" The use of "" requires constructing a std::string or dstringt, and then a string comparison. empty() is just an integer comparison (both for std::string an dstringt). --- jbmc/src/java_bytecode/expr2java.cpp | 3 +-- src/ansi-c/ansi_c_language.cpp | 2 +- src/ansi-c/ansi_c_parser.cpp | 2 +- src/ansi-c/expr2c.cpp | 3 +-- src/cpp/cpp_declarator_converter.cpp | 4 +--- src/cpp/cpp_language.cpp | 4 ++-- src/cpp/cpp_typecheck_namespace.cpp | 2 +- src/cpp/cpp_typecheck_resolve.cpp | 2 +- src/cpp/expr2cpp.cpp | 3 +-- src/goto-cc/compile.cpp | 2 +- src/goto-cc/gcc_mode.cpp | 5 +++-- src/goto-cc/ms_cl_cmdline.cpp | 2 +- src/goto-cc/ms_link_cmdline.cpp | 2 +- src/goto-checker/solver_factory.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 4 ++-- src/goto-instrument/wmm/weak_memory.cpp | 2 +- src/goto-programs/goto_trace.cpp | 2 +- src/goto-programs/json_goto_trace.cpp | 2 +- src/goto-programs/show_properties.cpp | 6 ++---- src/goto-programs/show_symbol_table.cpp | 8 ++++---- src/goto-programs/string_abstraction.cpp | 2 +- src/goto-symex/symex_main.cpp | 2 +- src/langapi/mode.cpp | 2 +- src/pointer-analysis/value_set.cpp | 6 +++--- src/pointer-analysis/value_set_fi.cpp | 4 ++-- src/pointer-analysis/value_set_fivr.cpp | 4 ++-- src/pointer-analysis/value_set_fivrns.cpp | 4 ++-- src/solvers/smt2/smt2_dec.cpp | 12 ++++++------ src/util/lispirep.cpp | 2 +- src/util/xml.cpp | 2 +- src/xmllang/xml_interface.cpp | 2 +- 31 files changed, 49 insertions(+), 55 deletions(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 7d51064204d..f298bfd999a 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -246,8 +246,7 @@ std::string expr2javat::convert_rec( qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); - const std::string d= - declarator==""?declarator:(" "+declarator); + const std::string d = declarator.empty() ? declarator : (" " + declarator); const std::string q= new_qualifiers.as_string(); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index acebc866760..1ff9c692b59 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -43,7 +43,7 @@ bool ansi_c_languaget::preprocess( std::ostream &outstream) { // stdin? - if(path=="") + if(path.empty()) return c_preprocess(instream, outstream, get_message_handler()); return c_preprocess(path, outstream, get_message_handler()); diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 7957b9fdd87..310a7e2bcb1 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -106,7 +106,7 @@ void ansi_c_parsert::add_declarator( } // global? - if(current_scope().prefix=="") + if(current_scope().prefix.empty()) ansi_c_declaration.set_is_global(true); // abstract? diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 7314f8acc79..5cae238158e 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -195,8 +195,7 @@ std::string expr2ct::convert_rec( std::string q=new_qualifiers.as_string(); - std::string d= - declarator==""?declarator:" "+declarator; + std::string d = declarator.empty() ? declarator : " " + declarator; if(src.find(ID_C_typedef).is_not_nil()) { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 894c82601a1..cfe7910aebe 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -397,9 +397,7 @@ void cpp_declarator_convertert::get_final_identifier() std::string identifier=id2string(base_name); // main is always "C" linkage, as a matter of principle - if(is_code && - base_name==ID_main && - scope->prefix=="") + if(is_code && base_name == ID_main && scope->prefix.empty()) { linkage_spec=ID_C; } diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index 88c1e4cd244..e0fb25e79c5 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -60,7 +60,7 @@ bool cpp_languaget::preprocess( const std::string &path, std::ostream &outstream) { - if(path=="") + if(path.empty()) return c_preprocess(instream, outstream, get_message_handler()); // check extension @@ -123,7 +123,7 @@ bool cpp_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { - if(module=="") + if(module.empty()) return false; symbol_tablet new_symbol_table; diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index a54d340ef91..082be2f2961 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -20,7 +20,7 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) const irep_idt &name=namespace_spec.get_namespace(); - if(name=="") + if(name.empty()) { // "unique namespace" error().source_location=namespace_spec.source_location(); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index c56fc46e5a3..e59f1ee6592 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -166,7 +166,7 @@ void cpp_typecheck_resolvet::remove_duplicates( else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag) id = to_union_tag_type(old_id.type()).get_identifier(); - if(id=="") + if(id.empty()) { if(other.insert(old_id).second) identifiers.push_back(old_id); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 04779993d96..cba5bb227f8 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -134,8 +134,7 @@ std::string expr2cppt::convert_rec( qualifierst &new_qualifiers = *clone; new_qualifiers.read(src); - const std::string d= - declarator==""?declarator:(" "+declarator); + const std::string d = declarator.empty() ? declarator : (" " + declarator); const std::string q= new_qualifiers.as_string(); diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index cc4c6b91f2b..e3a5cfec59f 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -389,7 +389,7 @@ bool compilet::compile() std::string cfn; - if(output_file_object=="") + if(output_file_object.empty()) { const std::string file_name_with_obj_ext = get_base_name(file_name, true) + "." + object_file_extension; diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 358708157dd..6d3d71c1693 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -683,8 +683,9 @@ int gcc_modet::doit() { compiler.add_input_file(arg_it->arg); } - else if(language=="c" || language=="c++" || - (language=="" && needs_preprocessing(arg_it->arg))) + else if( + language == "c" || language == "c++" || + (language.empty() && needs_preprocessing(arg_it->arg))) { std::string new_suffix; diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index 0dccb5587af..651d3870d3e 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/src/goto-cc/ms_cl_cmdline.cpp @@ -419,7 +419,7 @@ const char *ms_cl_prefixes[]= void ms_cl_cmdlinet::process_cl_option(const std::string &s) { - if(s=="") + if(s.empty()) return; if(s[0]!='/' && s[0]!='-') diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp index 543128d7897..187ed1b079d 100644 --- a/src/goto-cc/ms_link_cmdline.cpp +++ b/src/goto-cc/ms_link_cmdline.cpp @@ -325,7 +325,7 @@ static std::string to_upper_string(const std::string &s) void ms_link_cmdlinet::process_link_option(const std::string &s) { - if(s == "") + if(s.empty()) return; if(s[0] != '/' && s[0] != '-') diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 871d330f154..90b67d8de06 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -278,7 +278,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) const std::string &filename = options.get_option("outfile"); - if(filename == "") + if(filename.empty()) { if(solver == smt2_dect::solvert::GENERIC) { diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 06059ac7eba..4fec864be78 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1886,7 +1886,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) // none found? make one - if(id=="") + if(id.empty()) { irep_idt base_name=""; @@ -1900,7 +1900,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) base_name="nondet_"+id2string(suffix); } - if(base_name=="") + if(base_name.empty()) { unsigned count=0; while(symbol_table.symbols.find("nondet_"+std::to_string(count))!= diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 62c9d124773..bd2b9384f08 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -241,7 +241,7 @@ void weak_memory( const std::pair ran= shared_buffers.cycles_loc.equal_range(*it); for(m_itt ran_it=ran.first; ran_it!=ran.second; ran_it++) - message.result() << ((*it)==""?"fence":*it) << ", " + message.result() << (it->empty() ? "fence" : *it) << ", " << ran_it->second << messaget::eom; } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 9c5ada4d48e..44eaa6f81ae 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -229,7 +229,7 @@ std::string trace_numeric_value( forall_operands(it, expr) { - if(result=="") + if(result.empty()) result="{ "; else result+=", "; diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 02a6f0f128d..ca9267f84b5 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -126,7 +126,7 @@ void convert_decl( { base_name = symbol->base_name; display_name = symbol->display_name(); - if(type_string == "") + if(type_string.empty()) type_string = from_type(ns, identifier, symbol->type); json_assignment["mode"] = json_stringt(symbol->mode); diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index a8cf43df408..c9201da8369 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -61,8 +61,7 @@ void show_properties( const irep_idt &comment=source_location.get_comment(); const irep_idt &property_class=source_location.get_property_class(); - const irep_idt description= - (comment==""?"assertion":comment); + const irep_idt description = (comment.empty() ? "assertion" : comment); irep_idt property_id=source_location.get_property_id(); @@ -125,8 +124,7 @@ void convert_properties_json( const irep_idt &comment=source_location.get_comment(); // const irep_idt &function=location.get_function(); const irep_idt &property_class=source_location.get_property_class(); - const irep_idt description= - (comment==""?"assertion":comment); + const irep_idt description = (comment.empty() ? "assertion" : comment); irep_idt property_id=source_location.get_property_id(); diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 509904cd3ea..5ec68cd10d3 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -46,7 +46,7 @@ void show_symbol_table_brief_plain( std::unique_ptr ptr; - if(symbol.mode=="") + if(symbol.mode.empty()) ptr=get_default_language(); else { @@ -86,7 +86,7 @@ void show_symbol_table_plain( std::unique_ptr ptr; - if(symbol.mode=="") + if(symbol.mode.empty()) { ptr=get_default_language(); } @@ -174,7 +174,7 @@ static void show_symbol_table_json_ui( std::unique_ptr ptr; - if(symbol.mode=="") + if(symbol.mode.empty()) { ptr=get_default_language(); } @@ -248,7 +248,7 @@ static void show_symbol_table_brief_json_ui( std::unique_ptr ptr; - if(symbol.mode=="") + if(symbol.mode.empty()) { ptr=get_default_language(); } diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5b0f42400c4..ba9591daab9 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -169,7 +169,7 @@ void string_abstractiont::add_str_arguments( for(const auto &identifier : fct.parameter_identifiers) { - if(identifier=="") + if(identifier.empty()) continue; // ignore const symbolt ¶m_symbol = ns.lookup(identifier); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 3448d68a307..b018c4a20f2 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -100,7 +100,7 @@ void goto_symext::symex_assert( do_simplify(l2_condition); std::string msg = id2string(instruction.source_location.get_comment()); - if(msg == "") + if(msg.empty()) msg = "assertion"; vcc(l2_condition, msg, state); diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index b89d501d7d8..eab51721745 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -109,7 +109,7 @@ std::unique_ptr get_language_from_filename( std::string extension= std::string(filename, ext_pos+1, std::string::npos); - if(extension=="") + if(extension.empty()) return nullptr; for(languagest::const_iterator diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index ea002102d36..1846ad032e5 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -735,7 +735,7 @@ void value_sett::get_value_set_rec( } else if(statement==ID_allocate) { - assert(suffix==""); + PRECONDITION(suffix.empty()); const typet &dynamic_type= static_cast(expr.find(ID_C_cxx_alloc_type)); @@ -749,7 +749,7 @@ void value_sett::get_value_set_rec( else if(statement==ID_cpp_new || statement==ID_cpp_new_array) { - assert(suffix==""); + PRECONDITION(suffix.empty()); assert(expr_type.id()==ID_pointer); dynamic_object_exprt dynamic_object(expr_type.subtype()); @@ -1465,7 +1465,7 @@ void value_sett::do_function_call( it++) { const irep_idt &identifier=it->get_identifier(); - if(identifier=="") + if(identifier.empty()) continue; const exprt v_expr= diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 1325fc9bdb2..ca6ee909382 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -590,7 +590,7 @@ void value_set_fit::get_value_set_rec( if(expr.type().id()!=ID_pointer) throw "malloc expected to return pointer type"; - assert(suffix==""); + PRECONDITION(suffix.empty()); const typet &dynamic_type= static_cast(expr.find(ID_C_cxx_alloc_type)); @@ -607,7 +607,7 @@ void value_set_fit::get_value_set_rec( else if(statement==ID_cpp_new || statement==ID_cpp_new_array) { - assert(suffix==""); + PRECONDITION(suffix.empty()); assert(expr.type().id()==ID_pointer); dynamic_object_exprt dynamic_object(expr.type().subtype()); diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 526c3c20112..f38b26c8cc5 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -706,7 +706,7 @@ void value_set_fivrt::get_value_set_rec( if(expr.type().id()!=ID_pointer) throw "malloc expected to return pointer type"; - assert(suffix==""); + PRECONDITION(suffix.empty()); const typet &dynamic_type= static_cast(expr.find(ID_C_cxx_alloc_type)); @@ -723,7 +723,7 @@ void value_set_fivrt::get_value_set_rec( else if(statement==ID_cpp_new || statement==ID_cpp_new_array) { - assert(suffix==""); + PRECONDITION(suffix.empty()); assert(expr.type().id()==ID_pointer); dynamic_object_exprt dynamic_object(expr.type().subtype()); diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 654add1b4be..c60994f8c28 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -496,7 +496,7 @@ void value_set_fivrnst::get_value_set_rec( if(expr.type().id()!=ID_pointer) throw "malloc expected to return pointer type"; - assert(suffix==""); + PRECONDITION(suffix.empty()); const typet &dynamic_type= static_cast(expr.find(ID_C_cxx_alloc_type)); @@ -513,7 +513,7 @@ void value_set_fivrnst::get_value_set_rec( else if(statement==ID_cpp_new || statement==ID_cpp_new_array) { - assert(suffix==""); + PRECONDITION(suffix.empty()); assert(expr.type().id()==ID_pointer); dynamic_object_exprt dynamic_object(expr.type().subtype()); diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 0842df14734..487dc686fad 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -154,9 +154,9 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) res=resultt::D_SATISFIABLE; else if(parsed.id()=="unsat") res=resultt::D_UNSATISFIABLE; - else if(parsed.id()=="" && - parsed.get_sub().size()==1 && - parsed.get_sub().front().get_sub().size()==2) + else if( + parsed.id().empty() && parsed.get_sub().size() == 1 && + parsed.get_sub().front().get_sub().size() == 2) { const irept &s0=parsed.get_sub().front().get_sub()[0]; const irept &s1=parsed.get_sub().front().get_sub()[1]; @@ -169,9 +169,9 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) values[s0.id()]=s1; } - else if(parsed.id()=="" && - parsed.get_sub().size()==2 && - parsed.get_sub().front().id()=="error") + else if( + parsed.id().empty() && parsed.get_sub().size() == 2 && + parsed.get_sub().front().id() == "error") { // We ignore errors after UNSAT because get-value after check-sat // returns unsat will give an error. diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index ec42c2dbf58..890396ffc2d 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -32,7 +32,7 @@ void lisp2irep(const lispexprt &src, irept &dest) irept sub; lisp2irep(src[i], sub); - if(name=="") + if(name.empty()) dest.move_to_sub(sub); else dest.move_to_named_sub(name, sub); diff --git a/src/util/xml.cpp b/src/util/xml.cpp index bef696903c8..7b4104172a8 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -34,7 +34,7 @@ void xmlt::output(std::ostream &out, unsigned indent) const // 'name' needs to be set, or we produce mal-formed // XML. - if(name=="") + if(name.empty()) return; do_indent(out, indent); diff --git a/src/xmllang/xml_interface.cpp b/src/xmllang/xml_interface.cpp index a79e9aecc56..f29e26c47ad 100644 --- a/src/xmllang/xml_interface.cpp +++ b/src/xmllang/xml_interface.cpp @@ -32,7 +32,7 @@ static void get_xml_options(const xmlt &xml, cmdlinet &cmdline) std::string name = xml.get_attribute("name"); std::string value = xml.get_attribute("actual"); - if(name == "") + if(name.empty()) cmdline.args.push_back(value); else cmdline.set(name, value); From c1baa03b2e9bca49dfab801fb444ba94eb307c17 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 20:55:17 +0000 Subject: [PATCH 3/9] Remove redundant string initialisation Both std::string and dstringt are default-initialised to an empty string. --- jbmc/src/java_bytecode/expr2java.cpp | 2 +- src/analyses/local_may_alias.cpp | 2 +- src/cpp/cpp_typecheck_resolve.cpp | 2 +- src/goto-analyzer/show_on_source.cpp | 2 +- src/goto-instrument/dot.cpp | 2 +- src/goto-instrument/dump_c_class.h | 1 - src/goto-instrument/goto_program2code.cpp | 4 ++-- src/goto-programs/string_abstraction.cpp | 2 +- src/solvers/qbf/qbf_qube.cpp | 2 +- src/solvers/qbf/qbf_qube_core.cpp | 2 +- src/solvers/qbf/qbf_skizzo.cpp | 2 +- src/solvers/qbf/qbf_skizzo_core.cpp | 2 +- src/util/string_utils.cpp | 2 +- src/util/xml.cpp | 2 +- unit/json_symbol_table.cpp | 2 +- .../calculate_max_string_length.cpp | 2 +- unit/util/string_utils/split_string.cpp | 2 +- 17 files changed, 17 insertions(+), 18 deletions(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index f298bfd999a..4c7eb87d0eb 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -277,7 +277,7 @@ std::string expr2javat::convert_rec( // so we make one up, loosely inspired by the syntax // of lambda expressions. - std::string dest=""; + std::string dest; dest+='('; const java_method_typet::parameterst ¶meters = method_type.parameters(); diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index f853a6dced1..8da4c5edca2 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -458,7 +458,7 @@ void local_may_aliast::output( if(loc_info.aliases.find(j)==i) { assert(jis_goto()) { if(it->get_condition().is_true()) diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 10368d9e044..cacc03ee761 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -71,7 +71,6 @@ class dump_ct explicit typedef_infot(const irep_idt &name): typedef_name(name), - type_decl_str(""), early(false) { } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 4fec864be78..dac2387618a 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1864,7 +1864,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) // Replace by a function call to nondet_... // We first search for a suitable one in the symbol table. - irep_idt id=""; + irep_idt id; for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); @@ -1888,7 +1888,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) if(id.empty()) { - irep_idt base_name=""; + irep_idt base_name; if(expr.type().get(ID_C_c_type)!="") { diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index ba9591daab9..a6d0855e2ae 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -949,7 +949,7 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest) const typet &abstract_type=build_abstraction_type(symbol.type); CHECK_RETURN(!abstract_type.is_nil()); - irep_idt identifier=""; + irep_idt identifier; if(current_args.find(symbol.name)!=current_args.end()) identifier=id2string(symbol.name)+arg_suffix; diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp index c189c1d8f2e..2d853688a60 100644 --- a/src/solvers/qbf/qbf_qube.cpp +++ b/src/solvers/qbf/qbf_qube.cpp @@ -55,7 +55,7 @@ propt::resultt qbf_qubet::prop_solve() write_qdimacs_cnf(out); } - std::string options=""; + std::string options; // solve it int res=system( diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp index 291cbe69cf3..50a3927b6d6 100644 --- a/src/solvers/qbf/qbf_qube_core.cpp +++ b/src/solvers/qbf/qbf_qube_core.cpp @@ -51,7 +51,7 @@ propt::resultt qbf_qube_coret::prop_solve() write_qdimacs_cnf(out); } - std::string options=""; + std::string options; // solve it int res=system(( diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp index 5202e763d19..994c7d69650 100644 --- a/src/solvers/qbf/qbf_skizzo.cpp +++ b/src/solvers/qbf/qbf_skizzo.cpp @@ -55,7 +55,7 @@ propt::resultt qbf_skizzot::prop_solve() write_qdimacs_cnf(out); } - std::string options=""; + std::string options; // solve it int res=system(( diff --git a/src/solvers/qbf/qbf_skizzo_core.cpp b/src/solvers/qbf/qbf_skizzo_core.cpp index b1cb2ac4626..ed9a4da5ed6 100644 --- a/src/solvers/qbf/qbf_skizzo_core.cpp +++ b/src/solvers/qbf/qbf_skizzo_core.cpp @@ -68,7 +68,7 @@ propt::resultt qbf_skizzo_coret::prop_solve() write_qdimacs_cnf(out); } - std::string options=""; + std::string options; // solve it system(( diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 7e1c2b316e1..a081a9cc949 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -138,7 +138,7 @@ std::string trim_from_last_delimiter( const std::string &s, const char delim) { - std::string result=""; + std::string result; const size_t index=s.find_last_of(delim); if(index!=std::string::npos) result=s.substr(0, index); diff --git a/src/util/xml.cpp b/src/util/xml.cpp index 7b4104172a8..47221862e0d 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -213,7 +213,7 @@ void xmlt::set_attribute( /// \return the unescaped string std::string xmlt::unescape(const std::string &str) { - std::string result(""); + std::string result; result.reserve(str.size()); diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp index a72cbb1a7c8..9a475304323 100644 --- a/unit/json_symbol_table.cpp +++ b/unit/json_symbol_table.cpp @@ -59,7 +59,7 @@ void get_goto_model(std::istream &in, goto_modelt &goto_model) language_filest language_files; language_files.set_message_handler(null_message_handler); - std::string filename(""); + std::string filename; language_filet &language_file = language_files.add_file(filename); diff --git a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp index ef0d3dcfeaa..814bdfb00fe 100644 --- a/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp +++ b/unit/solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp @@ -16,7 +16,7 @@ Author: Diffblue Ltd. /// given radix. static size_t expected_length(unsigned long radix, const typet &type) { - std::string longest(""); + std::string longest; if(radix == 2) { if(type == unsignedbv_typet(32)) diff --git a/unit/util/string_utils/split_string.cpp b/unit/util/string_utils/split_string.cpp index bc7ef28cf95..bfc45d85485 100644 --- a/unit/util/string_utils/split_string.cpp +++ b/unit/util/string_utils/split_string.cpp @@ -107,7 +107,7 @@ SCENARIO("split_string", "[core][utils][string_utils][split_string]") } GIVEN("An empty string") { - std::string string = ""; + std::string string; WHEN("Splitting it") { expected_resultst expected_results; From 02105035440a22a432657fb50aea4bc8ecc3c7dd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 20:57:01 +0000 Subject: [PATCH 4/9] Use !s.empty() instead of s != "" The use of "" requires constructing a std::string or dstringt, and then a string comparison. empty() is just an integer comparison (both for std::string an dstringt). --- jbmc/unit/java-testing-utils/require_type.cpp | 2 +- src/analyses/invariant_set.cpp | 3 +-- src/ansi-c/expr2c.cpp | 16 ++++++++-------- src/cpp/cpp_constructor.cpp | 3 +-- src/cpp/cpp_destructor.cpp | 3 +-- src/cpp/cpp_type2name.cpp | 3 +-- src/cpp/cpp_typecheck_expr.cpp | 5 ++--- src/cpp/cpp_typecheck_resolve.cpp | 4 ++-- src/goto-cc/compile.cpp | 2 +- src/goto-cc/gcc_mode.cpp | 4 ++-- src/goto-instrument/call_sequences.cpp | 4 ++-- src/goto-instrument/dot.cpp | 15 +++++++-------- src/goto-instrument/goto_program2code.cpp | 2 +- src/goto-instrument/wmm/cycle_collection.cpp | 2 +- src/goto-programs/goto_function.cpp | 2 +- src/goto-programs/goto_program.cpp | 4 ++-- src/goto-programs/read_bin_goto_object.cpp | 2 +- src/goto-programs/set_properties.cpp | 6 +++--- src/goto-programs/vcd_goto_trace.cpp | 2 +- src/goto-programs/xml_goto_trace.cpp | 18 +++++++++--------- src/goto-symex/show_vcc.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_dereference_state.cpp | 6 ++---- src/linking/linking.cpp | 2 +- src/pointer-analysis/add_failed_symbols.cpp | 2 +- src/solvers/qbf/qbf_quantor.cpp | 2 +- src/solvers/qbf/qbf_qube.cpp | 2 +- src/solvers/qbf/qbf_qube_core.cpp | 2 +- src/solvers/qbf/qbf_skizzo.cpp | 2 +- src/solvers/qbf/qbf_skizzo_core.cpp | 6 +++--- .../string_constraint_generator_format.cpp | 2 +- src/util/get_module.cpp | 2 +- src/util/message.cpp | 10 +++++----- src/util/parser.cpp | 2 +- src/util/source_location.cpp | 10 +++++----- 35 files changed, 74 insertions(+), 82 deletions(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 9c8e682fa8b..019a73efcb1 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -470,7 +470,7 @@ require_type::require_struct_tag(const typet &type, const irep_idt &identifier) { REQUIRE(type.id() == ID_struct_tag); const struct_tag_typet &result = to_struct_tag_type(type); - if(identifier != "") + if(!identifier.empty()) { REQUIRE(result.get_identifier() == identifier); } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index 2f61a3ae460..da88a2dc5ba 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -63,8 +63,7 @@ bool inv_object_storet::get(const exprt &expr, unsigned &n) unsigned inv_object_storet::add(const exprt &expr) { std::string s=build_string(expr); - - assert(s!=""); + CHECK_RETURN(!s.empty()); mapt::number_type n=map.number(s); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5cae238158e..02e633d75a0 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -336,7 +336,7 @@ std::string expr2ct::convert_rec( std::string dest=q+"union"; const irep_idt &tag=union_type.get_tag(); - if(tag!="") + if(!tag.empty()) dest+=" "+id2string(tag); if(!union_type.is_incomplete()) @@ -420,7 +420,7 @@ std::string expr2ct::convert_rec( // The star gets attached to the declarator. std::string new_declarator="*"; - if(q != "" && (!declarator.empty() || subtype.id() == ID_pointer)) + if(!q.empty() && (!declarator.empty() || subtype.id() == ID_pointer)) { new_declarator+=" "+q; } @@ -448,7 +448,7 @@ std::string expr2ct::convert_rec( std::string dest=q+"struct"; const std::string &tag=ns.follow_tag(struct_tag_type).get_string(ID_tag); - if(tag!="") + if(!tag.empty()) dest+=" "+tag; dest+=d; @@ -461,7 +461,7 @@ std::string expr2ct::convert_rec( std::string dest=q+"union"; const std::string &tag=ns.follow_tag(union_tag_type).get_string(ID_tag); - if(tag!="") + if(!tag.empty()) dest+=" "+tag; dest+=d; @@ -641,7 +641,7 @@ std::string expr2ct::convert_struct_type( std::string dest=qualifiers+"struct"; const irep_idt &tag=struct_type.get_tag(); - if(tag!="") + if(!tag.empty()) dest+=" "+id2string(tag); if(inc_struct_body && !struct_type.is_incomplete()) @@ -1529,7 +1529,7 @@ std::string expr2ct::convert_member( irep_idt component_name=src.get_component_name(); - if(component_name!="") + if(!component_name.empty()) { const exprt &comp_expr = struct_union_type.get_component(component_name); @@ -1824,7 +1824,7 @@ std::string expr2ct::convert_constant( { dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string(); - if(dest!="" && isdigit(dest[dest.size()-1])) + if(!dest.empty() && isdigit(dest[dest.size() - 1])) { if(dest.find('.')==std::string::npos) dest+=".0"; @@ -1878,7 +1878,7 @@ std::string expr2ct::convert_constant( { dest=fixedbvt(to_constant_expr(src)).to_ansi_c_string(); - if(dest!="" && isdigit(dest[dest.size()-1])) + if(!dest.empty() && isdigit(dest[dest.size() - 1])) { if(src.type()==float_type()) dest+='f'; diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index cb3830c78ce..7f8b4981bc6 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -218,8 +218,7 @@ optionalt cpp_typecheckt::cpp_constructor( } } - // there is always a constructor for non-PODs - assert(constructor_name!=""); + INVARIANT(!constructor_name.empty(), "non-PODs should have a constructor"); side_effect_expr_function_callt function_call( cpp_namet(constructor_name, source_location).as_expr(), diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index f6e2ac0f500..a0f32d708d3 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -97,8 +97,7 @@ optionalt cpp_typecheckt::cpp_destructor( } } - // there is always a destructor for non-PODs - assert(dtor_name!=""); + INVARIANT(!dtor_name.empty(), "non-PODs should have a destructor"); cpp_namet cpp_name(dtor_name, source_location); diff --git a/src/cpp/cpp_type2name.cpp b/src/cpp/cpp_type2name.cpp index 134a3c92d12..dc45e96a3bd 100644 --- a/src/cpp/cpp_type2name.cpp +++ b/src/cpp/cpp_type2name.cpp @@ -19,8 +19,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu static std::string do_prefix(const std::string &s) { - if(s.find(',')!=std::string::npos || - (s!="" && isdigit(s[0]))) + if(s.find(',') != std::string::npos || (!s.empty() && isdigit(s[0]))) return std::to_string(s.size())+"_"+s; return s; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 432bc072f36..2e3005225cb 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1198,8 +1198,7 @@ void cpp_typecheckt::typecheck_expr_member( } const irep_idt &component_name=expr.get(ID_component_name); - - assert(component_name!=""); + INVARIANT(!component_name.empty(), "component name should not be empty"); exprt component; component.make_nil(); @@ -2131,7 +2130,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( // special case for the initialization of parents if(member.get_bool(ID_C_not_accessible)) { - assert(member.get(ID_C_access)!=""); + PRECONDITION(!member.get(ID_C_access).empty()); tmp_object_expr.set(ID_C_not_accessible, true); tmp_object_expr.set(ID_C_access, member.get(ID_C_access)); } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 49bf743bc49..6f28e666b83 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -446,7 +446,7 @@ void cpp_typecheck_resolvet::disambiguate_functions( { std::size_t template_distance=0; - if(old_id.type().get(ID_C_template) != "") + if(!old_id.type().get(ID_C_template).empty()) template_distance = old_id.type() .find(ID_C_template_arguments) .find(ID_arguments) @@ -1011,7 +1011,7 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( if(!cpp_declaration.is_class_template()) continue; irep_idt specialization_of=cpp_declaration.get_specialization_of(); - if(specialization_of!="") + if(!specialization_of.empty()) primary_templates.insert(specialization_of); else primary_templates.insert(id); diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index e3a5cfec59f..0513d1c1f8f 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -433,7 +433,7 @@ bool compilet::parse( // Using '-x', the type of a file can be overridden; // otherwise, it's guessed from the extension. - if(override_language!="") + if(!override_language.empty()) { if(override_language=="c++" || override_language=="c++-header") languagep = get_language_from_mode(ID_cpp); diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 6d3d71c1693..966821914e6 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -484,7 +484,7 @@ int gcc_modet::doit() cmdline.isset("mtune") ? cmdline.get_value("mtune") : cmdline.isset("mcpu") ? cmdline.get_value("mcpu") : ""; - if(target_cpu!="") + if(!target_cpu.empty()) { // Work out what CPROVER architecture we should target. for(auto &pair : arch_map) @@ -821,7 +821,7 @@ int gcc_modet::preprocess( } // language, if given - if(language!="") + if(!language.empty()) { new_argv.push_back("-x"); new_argv.push_back(language); diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 769223a09b4..ac286bae658 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -258,10 +258,10 @@ void check_call_sequence(const goto_modelt &goto_model) std::string line; while(std::getline(std::cin, line)) { - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); - if(line!="") + if(!line.empty()) sequence.push_back(line); } diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index aa1ee47109e..3c179705674 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -338,14 +338,13 @@ void dott::write_edge( out << "Node_" << subgraphscount << "_" << from.location_number; out << " -> "; out << "Node_" << subgraphscount << "_" << to.location_number << " "; - if(label!="") - { - out << "[fontsize=20,label=\"" << label << "\""; - if(from.is_backwards_goto() && - from.location_number > to.location_number) - out << ",color=red"; - out << "]"; - } + if(!label.empty()) + { + out << "[fontsize=20,label=\"" << label << "\""; + if(from.is_backwards_goto() && from.location_number > to.location_number) + out << ",color=red"; + out << "]"; + } out << ";\n"; } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index dac2387618a..c822e2e843a 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1890,7 +1890,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) { irep_idt base_name; - if(expr.type().get(ID_C_c_type)!="") + if(!expr.type().get(ID_C_c_type).empty()) { irep_idt suffix; suffix=expr.type().get(ID_C_c_type); diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp index 5d7a919677d..b6c1c3f1795 100644 --- a/src/goto-instrument/wmm/cycle_collection.cpp +++ b/src/goto-instrument/wmm/cycle_collection.cpp @@ -211,7 +211,7 @@ bool event_grapht::graph_explorert::backtrack( cycle cannot be with x */ irep_idt avoid_at_the_end=var_to_avoid; bool no_comm=false; - if(avoid_at_the_end!="" && avoid_at_the_end==this_vertex.variable) + if(!avoid_at_the_end.empty() && avoid_at_the_end == this_vertex.variable) no_comm=true; /* if specified, maximum number of events reached */ diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index 3d86edcded8..6fa8480a791 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -24,7 +24,7 @@ void get_local_identifiers( // add parameters for(const auto &identifier : goto_function.parameter_identifiers) { - if(identifier != "") + if(!identifier.empty()) dest.insert(identifier); } } diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 0416af0bb25..df335b3af0f 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -115,7 +115,7 @@ std::ostream &goto_programt::output_instruction( out << from_expr(ns, identifier, instruction.get_condition()); const irep_idt &comment=instruction.source_location.get_comment(); - if(comment!="") + if(!comment.empty()) out << " // " << comment; } @@ -453,7 +453,7 @@ std::string as_string( { const irep_idt &comment=i.source_location.get_comment(); - if(comment!="") + if(!comment.empty()) result+=" /* "+id2string(comment)+" */"; } return result; diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 09fbebd9a53..8bdf7929eeb 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -207,7 +207,7 @@ bool read_bin_goto_object( } else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F') { - if(filename!="") + if(!filename.empty()) message.error() << "Sorry, but I can't read ELF binary `" << filename << "'" << messaget::eom; else diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 1ae461b883f..91687341077 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -60,9 +60,9 @@ void label_properties( irep_idt function=it->source_location.get_function(); std::string prefix=id2string(function); - if(it->source_location.get_property_class()!="") + if(!it->source_location.get_property_class().empty()) { - if(prefix!="") + if(!prefix.empty()) prefix+="."; std::string class_infix= @@ -74,7 +74,7 @@ void label_properties( prefix+=class_infix; } - if(prefix!="") + if(!prefix.empty()) prefix+="."; std::size_t &count=property_counters[prefix]; diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 7bc890309c0..1a076fbab41 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -142,7 +142,7 @@ void output_vcd( { std::string binary=as_vcd_binary(step.full_lhs_value, ns); - if(binary!="") + if(!binary.empty()) out << "b" << binary << " V" << number << " " << "\n"; } } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 4af88697d0f..c6c88f2ad41 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -37,7 +37,7 @@ void convert( const source_locationt &source_location=step.pc->source_location; xmlt xml_location; - if(source_location.is_not_nil() && source_location.get_file()!="") + if(source_location.is_not_nil() && !source_location.get_file().empty()) xml_location=xml(source_location); switch(step.type) @@ -53,7 +53,7 @@ void convert( xml_failure.set_attribute("reason", id2string(step.comment)); xml_failure.set_attribute("property", id2string(step.property_id)); - if(xml_location.name!="") + if(!xml_location.name.empty()) xml_failure.new_element().swap(xml_location); } break; @@ -66,7 +66,7 @@ void convert( lhs_object.has_value()?lhs_object->get_identifier():irep_idt(); xmlt &xml_assignment=dest.new_element("assignment"); - if(xml_location.name!="") + if(!xml_location.name.empty()) xml_assignment.new_element().swap(xml_location); { @@ -121,7 +121,7 @@ void convert( xml_output.set_attribute("thread", std::to_string(step.thread_nr)); xml_output.set_attribute("step_nr", std::to_string(step.step_nr)); - if(xml_location.name!="") + if(!xml_location.name.empty()) xml_output.new_element().swap(xml_location); for(const auto &arg : step.io_args) @@ -151,7 +151,7 @@ void convert( new_element(xml(arg, ns)); } - if(xml_location.name!="") + if(!xml_location.name.empty()) xml_input.new_element().swap(xml_location); } break; @@ -172,7 +172,7 @@ void convert( xml_function.set_attribute("identifier", id2string(symbol.name)); xml_function.new_element() = xml(symbol.location); - if(xml_location.name != "") + if(!xml_location.name.empty()) xml_call_return.new_element().swap(xml_location); } break; @@ -193,7 +193,7 @@ void convert( xml_function.set_attribute("identifier", id2string(symbol.name)); xml_function.new_element()=xml(symbol.location); - if(xml_location.name!="") + if(!xml_location.name.empty()) xml_call_return.new_element().swap(xml_location); } break; @@ -202,7 +202,7 @@ void convert( if(source_location!=previous_source_location) { // just the source location - if(xml_location.name!="") + if(!xml_location.name.empty()) { xmlt &xml_location_only=dest.new_element("location-only"); @@ -217,7 +217,7 @@ void convert( } } - if(source_location.is_not_nil() && source_location.get_file()!="") + if(source_location.is_not_nil() && !source_location.get_file().empty()) previous_source_location=source_location; } } diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp index bee00acdd42..3e0fa1ea05a 100644 --- a/src/goto-symex/show_vcc.cpp +++ b/src/goto-symex/show_vcc.cpp @@ -48,7 +48,7 @@ show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation) if(s_it->source.pc->source_location.is_not_nil()) out << s_it->source.pc->source_location << '\n'; - if(s_it->comment != "") + if(!s_it->comment.empty()) out << s_it->comment << '\n'; symex_target_equationt::SSA_stepst::const_iterator p_it = diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 54dc1d9e245..f2d12802a55 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -323,7 +323,7 @@ void goto_symext::symex_printf( const irep_idt format_string= get_string_argument(operands[0], ns); - if(format_string!="") + if(!format_string.empty()) target.output_fmt( state.guard.as_expr(), state.source, "printf", format_string, args); diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp index ae77f3237b7..495a5ac956f 100644 --- a/src/goto-symex/symex_dereference_state.cpp +++ b/src/goto-symex/symex_dereference_state.cpp @@ -43,8 +43,7 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr) const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol); const symbolt *symbol; - if(failed_symbol!="" && - !ns.lookup(failed_symbol, symbol)) + if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol)) { symbolt sym=*symbol; symbolt *sym_ptr=nullptr; @@ -63,8 +62,7 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr) const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol); const symbolt *symbol; - if(failed_symbol!="" && - !ns.lookup(failed_symbol, symbol)) + if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol)) { symbolt sym=*symbol; symbolt *sym_ptr=nullptr; diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 55be33856ec..2fc133295aa 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -79,7 +79,7 @@ std::string linkingt::type_to_string_verbose( std::string result=followed.id_string(); const std::string &tag=followed.get_string(ID_tag); - if(tag!="") + if(!tag.empty()) result+=" "+tag; if(to_struct_union_type(followed).is_incomplete()) diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index fc93e1d3f6c..49efb89f841 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -64,7 +64,7 @@ void add_failed_symbol_if_needed( if(!symbol.is_lvalue) return; - if(symbol.type.get(ID_C_failed_symbol)!="") + if(!symbol.type.get(ID_C_failed_symbol).empty()) return; add_failed_symbol(symbol_table.get_writeable_ref(symbol.name), symbol_table); diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp index 8c2e7969982..4ee783f2674 100644 --- a/src/solvers/qbf/qbf_quantor.cpp +++ b/src/solvers/qbf/qbf_quantor.cpp @@ -67,7 +67,7 @@ propt::resultt qbf_quantort::prop_solve() std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line=="s TRUE") diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp index 2d853688a60..0c0eedaff1d 100644 --- a/src/solvers/qbf/qbf_qube.cpp +++ b/src/solvers/qbf/qbf_qube.cpp @@ -75,7 +75,7 @@ propt::resultt qbf_qubet::prop_solve() std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line=="s cnf 0") diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp index 50a3927b6d6..8b612240382 100644 --- a/src/solvers/qbf/qbf_qube_core.cpp +++ b/src/solvers/qbf/qbf_qube_core.cpp @@ -71,7 +71,7 @@ propt::resultt qbf_qube_coret::prop_solve() std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line[0]=='V') diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp index 994c7d69650..2dcaa56bc6d 100644 --- a/src/solvers/qbf/qbf_skizzo.cpp +++ b/src/solvers/qbf/qbf_skizzo.cpp @@ -75,7 +75,7 @@ propt::resultt qbf_skizzot::prop_solve() std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line=="The instance evaluates to TRUE.") diff --git a/src/solvers/qbf/qbf_skizzo_core.cpp b/src/solvers/qbf/qbf_skizzo_core.cpp index ed9a4da5ed6..d4be0851029 100644 --- a/src/solvers/qbf/qbf_skizzo_core.cpp +++ b/src/solvers/qbf/qbf_skizzo_core.cpp @@ -87,7 +87,7 @@ propt::resultt qbf_skizzo_coret::prop_solve() std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line=="The instance evaluates to TRUE.") @@ -161,7 +161,7 @@ bool qbf_skizzo_coret::get_certificate(void) std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line.compare(0, key.size(), key)==0) @@ -205,7 +205,7 @@ bool qbf_skizzo_coret::get_certificate(void) { std::getline(in, line); - if(line!="" && line[line.size()-1]=='\r') + if(!line.empty() && line[line.size() - 1] == '\r') line.resize(line.size()-1); if(line.compare(0, key.size(), key)==0) diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp index c71a3a08573..cb35a53278c 100644 --- a/src/solvers/strings/string_constraint_generator_format.cpp +++ b/src/solvers/strings/string_constraint_generator_format.cpp @@ -199,7 +199,7 @@ static format_specifiert format_specifier_of_match(std::smatch &m) int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str()); std::string tT = m[5].str(); - bool dt = (tT != ""); + bool dt = !tT.empty(); if(tT == "T") flag.push_back(format_specifiert::DATE_TIME_UPPER); diff --git a/src/util/get_module.cpp b/src/util/get_module.cpp index b53196c1391..376cab2adc3 100644 --- a/src/util/get_module.cpp +++ b/src/util/get_module.cpp @@ -77,7 +77,7 @@ const symbolt &get_module( const std::string &module, message_handlert &message_handler) { - if(module!="") + if(!module.empty()) return get_module_by_name(symbol_table, module, message_handler); symbolptr_listt symbolptr_list, main_symbolptr_list; diff --git a/src/util/message.cpp b/src/util/message.cpp index fd740117a69..251f4a6dab5 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -26,30 +26,30 @@ void message_handlert::print( if(!file.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="file "+id2string(file); } if(!line.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="line "+id2string(line); } if(!column.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="column "+id2string(column); } if(!function.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="function "+id2string(function); } - if(dest!="") + if(!dest.empty()) dest+=": "; dest+=message; diff --git a/src/util/parser.cpp b/src/util/parser.cpp index dffdb151c02..b2a846e932a 100644 --- a/src/util/parser.cpp +++ b/src/util/parser.cpp @@ -32,7 +32,7 @@ void parsert::parse_error( const std::string &before) { std::string tmp=message; - if(before!="") + if(!before.empty()) tmp+=" before `"+before+"'"; #if 0 diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 73b841c319f..499f3809a92 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -33,7 +33,7 @@ std::string source_locationt::as_string(bool print_cwd) const if(!file.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="file "; if(print_cwd) @@ -44,25 +44,25 @@ std::string source_locationt::as_string(bool print_cwd) const } if(!line.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="line "+id2string(line); } if(!column.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="column "+id2string(column); } if(!function.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="function "+id2string(function); } if(!bytecode.empty()) { - if(dest!="") + if(!dest.empty()) dest+=' '; dest+="bytecode-index "+id2string(bytecode); } From 8a277eff2b917a0805cc47742a2591fd2c8b83be Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 20:58:08 +0000 Subject: [PATCH 5/9] Use irep_idt() instead of "" Constructing a dstringt from a C string requires a string table lookup, while the default constructor for a dstringt just zero-initialises an unsigned. --- .../java_string_library_preprocess.cpp | 2 +- src/analyses/ai.h | 10 +++--- src/analyses/goto_rw.cpp | 2 +- src/analyses/invariant_set.cpp | 10 +++--- src/analyses/local_bitvector_analysis.cpp | 2 +- src/analyses/local_may_alias.cpp | 2 +- src/analyses/local_safe_pointers.cpp | 4 +-- src/analyses/static_analysis.h | 2 +- src/ansi-c/c_preprocess.cpp | 4 +-- .../accelerate/acceleration_utils.cpp | 4 +-- .../accelerate/polynomial_accelerator.cpp | 4 +-- src/goto-instrument/wmm/cycle_collection.cpp | 36 +++++++++++-------- src/goto-programs/goto_inline_class.cpp | 2 +- src/goto-programs/goto_program.h | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_dereference_state.cpp | 4 +-- src/jsil/jsil_language.cpp | 2 +- src/langapi/language_util.cpp | 6 ++-- src/linking/linking.cpp | 4 +-- src/util/expr_initializer.cpp | 2 +- 20 files changed, 57 insertions(+), 49 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index cfba5175196..465359614cd 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -41,7 +41,7 @@ static irep_idt get_tag(const typet &type) else if(type.id() == ID_struct) return irep_idt("java::" + id2string(to_struct_type(type).get_tag())); else - return ""; + return irep_idt(); } /// \param type: a type diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 97ded96fc6f..d1c4ce05468 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -157,7 +157,7 @@ class ai_baset const goto_functionst::goto_functiont &goto_function, std::ostream &out) const { - output(ns, "", goto_function.body, out); + output(ns, irep_idt(), goto_function.body, out); } /// Output the abstract states for the whole program as JSON @@ -178,7 +178,7 @@ class ai_baset const namespacet &ns, const goto_programt &goto_program) const { - return output_json(ns, "", goto_program); + return output_json(ns, irep_idt(), goto_program); } /// Output the abstract states for a single function as JSON @@ -186,7 +186,7 @@ class ai_baset const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const { - return output_json(ns, "", goto_function.body); + return output_json(ns, irep_idt(), goto_function.body); } /// Output the abstract states for the whole program as XML @@ -207,7 +207,7 @@ class ai_baset const namespacet &ns, const goto_programt &goto_program) const { - return output_xml(ns, "", goto_program); + return output_xml(ns, irep_idt(), goto_program); } /// Output the abstract states for a single function as XML @@ -215,7 +215,7 @@ class ai_baset const namespacet &ns, const goto_functionst::goto_functiont &goto_function) const { - return output_xml(ns, "", goto_function.body); + return output_xml(ns, irep_idt(), goto_function.body); } protected: diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index dc4eb49b089..6f3a9954628 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -671,7 +671,7 @@ void guarded_range_domaint::output( out << itr->first << ":" << itr->second.first; // we don't know what mode (language) we are in, so we rely on the default // language to be reasonable for from_expr - out << " if " << from_expr(ns, "", itr->second.second); + out << " if " << from_expr(ns, irep_idt(), itr->second.second); } out << "]"; } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index da88a2dc5ba..97f99e00808 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -136,7 +136,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const // we don't know what mode (language) we are in, so we rely on the default // language to be reasonable for from_expr if(is_constant_address(expr)) - return from_expr(ns, "", expr); + return from_expr(ns, irep_idt(), expr); if(expr.id()==ID_member) { @@ -390,8 +390,8 @@ void invariant_sett::strengthen_rec(const exprt &expr) throw "non-Boolean argument to strengthen()"; #if 0 - std::cout << "S: " << from_expr(*ns, "", expr) << '\n'; - #endif + std::cout << "S: " << from_expr(*ns, irep_idt(), expr) << '\n'; +#endif if(is_false) { @@ -593,8 +593,8 @@ tvt invariant_sett::implies_rec(const exprt &expr) const throw "implies: non-Boolean expression"; #if 0 - std::cout << "I: " << from_expr(*ns, "", expr) << '\n'; - #endif + std::cout << "I: " << from_expr(*ns, irep_idt(), expr) << '\n'; +#endif if(is_false) // can't get any stronger return tvt(true); diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 84117cbe903..bddd6cd4384 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -347,7 +347,7 @@ void local_bitvector_analysist::output( } out << "\n"; - goto_function.body.output_instruction(ns, "", out, *i_it); + goto_function.body.output_instruction(ns, irep_idt(), out, *i_it); out << "\n"; l++; diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 8da4c5edca2..4b4266f65dc 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -470,7 +470,7 @@ void local_may_aliast::output( } out << "\n"; - goto_function.body.output_instruction(ns, "", out, *i_it); + goto_function.body.output_instruction(ns, irep_idt(), out, *i_it); out << "\n"; l++; diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index f76003db2ba..491d1a3d16f 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -207,7 +207,7 @@ void local_safe_pointerst::output( } out << '\n'; - goto_program.output_instruction(ns, "", out, *i_it); + goto_program.output_instruction(ns, irep_idt(), out, *i_it); out << '\n'; } } @@ -258,7 +258,7 @@ void local_safe_pointerst::output_safe_dereferences( } out << '\n'; - goto_program.output_instruction(ns, "", out, *i_it); + goto_program.output_instruction(ns, irep_idt(), out, *i_it); out << '\n'; } } diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h index a3e3a0e8a8b..72898bfd328 100644 --- a/src/analyses/static_analysis.h +++ b/src/analyses/static_analysis.h @@ -155,7 +155,7 @@ class static_analysis_baset const goto_programt &goto_program, std::ostream &out) const { - output(goto_program, "", out); + output(goto_program, irep_idt(), out); } virtual bool has_location(locationt l) const=0; diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index 5a7be8ebce3..aa827cf3df3 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -200,9 +200,9 @@ static void error_parse_line( if(state==2) { saved_error_location.set_file(file); - saved_error_location.set_function(""); + saved_error_location.set_function(irep_idt()); saved_error_location.set_line(line_no); - saved_error_location.set_column(""); + saved_error_location.set_column(irep_idt()); } } diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index b7a24db499f..e718914a0e8 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -157,7 +157,7 @@ bool acceleration_utilst::check_inductive( #ifdef DEBUG std::cout << "Checking following program for inductiveness:\n"; - program.output(ns, "", std::cout); + program.output(ns, irep_idt(), std::cout); #endif try @@ -440,7 +440,7 @@ bool acceleration_utilst::do_assumptions( #ifdef DEBUG std::cout << "Checking following program for monotonicity:\n"; - program.output(ns, "", std::cout); + program.output(ns, irep_idt(), std::cout); #endif try diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index e1cba8afb0b..07e851843eb 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -403,7 +403,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced( #ifdef DEBUG std::cout << "Fitting polynomial with program:\n"; - program.output(ns, "", std::cout); + program.output(ns, irep_idt(), std::cout); #endif // Now do an ASSERT(false) to grab a counterexample @@ -699,7 +699,7 @@ bool polynomial_acceleratort::check_inductive( #ifdef DEBUG std::cout << "Checking following program for inductiveness:\n"; - program.output(ns, "", std::cout); + program.output(ns, irep_idt(), std::cout); #endif try diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp index b6c1c3f1795..7b55a74e7c5 100644 --- a/src/goto-instrument/wmm/cycle_collection.cpp +++ b/src/goto-instrument/wmm/cycle_collection.cpp @@ -89,8 +89,17 @@ void event_grapht::graph_explorert::collect_cycles( { event_idt source=*st_it; egraph.message.debug() << "explore " << egraph[source].id << messaget::eom; - backtrack(set_of_cycles, source, source, - false, max_po_trans, false, false, false, "", model); + backtrack( + set_of_cycles, + source, + source, + false, + max_po_trans, + false, + false, + false, + irep_idt(), + model); while(!marked_stack.empty()) { @@ -452,18 +461,17 @@ bool event_grapht::graph_explorert::backtrack( f=true; } else if(!mark[w]) - f|= - backtrack( - set_of_cycles, - source, - w, - unsafe_met_updated, - po_trans, - false, - false, - false, - "", - model); + f |= backtrack( + set_of_cycles, + source, + w, + unsafe_met_updated, + po_trans, + false, + false, + false, + irep_idt(), + model); } } diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index f0eaaa678f0..8808d8d4869 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -331,7 +331,7 @@ void goto_inlinet::expand_function_call( #ifdef DEBUG std::cout << "Expanding call:\n"; - dest.output_instruction(ns, "", std::cout, *target); + dest.output_instruction(ns, irep_idt(), std::cout, *target); #endif exprt lhs; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 4e84eaf191f..0cff59cd9a5 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -712,7 +712,7 @@ class goto_programt /// Output goto-program to given stream std::ostream &output(std::ostream &out) const { - return output(namespacet(symbol_tablet()), "", out); + return output(namespacet(symbol_tablet()), irep_idt(), out); } /// Output a single instruction diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index f2d12802a55..4bbd2a43d81 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -295,7 +295,7 @@ irep_idt get_string_argument_rec(const exprt &src) } } - return ""; + return irep_idt(); } irep_idt get_string_argument(const exprt &src, const namespacet &ns) diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp index 495a5ac956f..1513df0f264 100644 --- a/src/goto-symex/symex_dereference_state.cpp +++ b/src/goto-symex/symex_dereference_state.cpp @@ -91,7 +91,7 @@ void symex_dereference_statet::get_value_set( #endif #if 0 - std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n'; + std::cout << "E: " << from_expr(goto_symex.ns, irep_idt(), expr) << '\n'; #endif #if 0 @@ -99,7 +99,7 @@ void symex_dereference_statet::get_value_set( for(value_setst::valuest::const_iterator it=value_set.begin(); it!=value_set.end(); it++) - std::cout << from_expr(goto_symex.ns, "", *it) << '\n'; + std::cout << from_expr(goto_symex.ns, irep_idt(), *it) << '\n'; std::cout << "**************************\n"; #endif } diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index ad86320e3e7..1ab3a9b4821 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -134,7 +134,7 @@ bool jsil_languaget::to_expr( // parsing jsil_parser.clear(); - jsil_parser.set_file(""); + jsil_parser.set_file(irep_idt()); jsil_parser.in=&instream; jsil_parser.set_message_handler(get_message_handler()); jsil_scanner_init(); diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 87c51c9877f..a471cd5c652 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -59,13 +59,13 @@ std::string type_to_name( std::string from_expr(const exprt &expr) { symbol_tablet symbol_table; - return from_expr(namespacet(symbol_table), "", expr); + return from_expr(namespacet(symbol_table), irep_idt(), expr); } std::string from_type(const typet &type) { symbol_tablet symbol_table; - return from_type(namespacet(symbol_table), "", type); + return from_type(namespacet(symbol_table), irep_idt(), type); } exprt to_expr( @@ -91,5 +91,5 @@ exprt to_expr( std::string type_to_name(const typet &type) { symbol_tablet symbol_table; - return type_to_name(namespacet(symbol_table), "", type); + return type_to_name(namespacet(symbol_table), irep_idt(), type); } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 2fc133295aa..18b25d069c9 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -359,8 +359,8 @@ void linkingt::detailed_conflict_report_rec( if(!msg.empty()) { error() << '\n'; - error() << "reason for conflict at " << expr_to_string("", conflict_path) - << ": " << msg << '\n'; + error() << "reason for conflict at " + << expr_to_string(irep_idt(), conflict_path) << ": " << msg << '\n'; error() << '\n'; error() << type_to_string_verbose(old_symbol, t1) << '\n'; diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 049dc60fa5a..ca3984549f2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -242,7 +242,7 @@ optionalt expr_initializert::expr_initializer_rec( if(!found) { // stupid empty union - union_exprt value("", nil_exprt(), type); + union_exprt value(irep_idt(), nil_exprt(), type); value.add_source_location() = source_location; return std::move(value); } From 672e71196540f4d10e8079207eaab7766c802526 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 21:00:15 +0000 Subject: [PATCH 6/9] The second argument to java_type_from_string is optional --- jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp index aaf4dc6fb6f..e3143b95263 100644 --- a/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp +++ b/jbmc/unit/java_bytecode/java_types/java_type_from_string.cpp @@ -15,7 +15,7 @@ SCENARIO("java_type_from_string", "[core][java_types]") GIVEN("Ljava/lang/Integer;") { - const auto integer_type = java_type_from_string("Ljava/lang/Integer;", ""); + const auto integer_type = java_type_from_string("Ljava/lang/Integer;"); REQUIRE(integer_type.has_value()); } @@ -35,7 +35,7 @@ SCENARIO("java_type_from_string", "[core][java_types]") GIVEN("Ljava/util/List;") { const auto integer_list_type = - java_type_from_string("Ljava/util/List;", ""); + java_type_from_string("Ljava/util/List;"); REQUIRE(integer_list_type.has_value()); } From 7e5b60fb6909176f3525bc16b68a4d37bd3119d0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 21:01:29 +0000 Subject: [PATCH 7/9] Use s.clear() instead of s="" This avoids string table lookups. --- src/ansi-c/expr2c.cpp | 10 +++++----- src/cpp/cpp_name.cpp | 2 +- src/cpp/cpp_token.h | 4 ++-- src/cpp/cpp_typecheck_resolve.cpp | 2 +- src/goto-cc/armcc_mode.cpp | 2 +- src/goto-cc/cw_mode.cpp | 2 +- src/goto-cc/gcc_mode.cpp | 6 +++--- src/goto-cc/ld_mode.cpp | 2 +- src/goto-cc/ms_cl_cmdline.cpp | 4 ++-- src/goto-instrument/dump_c.cpp | 4 ++-- src/pointer-analysis/value_set.cpp | 4 ++-- src/pointer-analysis/value_set_fi.cpp | 2 +- src/util/cmdline.cpp | 4 ++-- src/util/identifier.cpp | 2 +- src/util/lispexpr.cpp | 4 ++-- src/util/lispirep.cpp | 4 ++-- 16 files changed, 29 insertions(+), 29 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 02e633d75a0..efc07cc8dd5 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -287,13 +287,13 @@ std::string expr2ct::convert_rec( if(width==config.ansi_c.int_width) { if(is_signed) - sign_str=""; + sign_str.clear(); return q+sign_str+"int"+d; } else if(width==config.ansi_c.long_int_width) { if(is_signed) - sign_str=""; + sign_str.clear(); return q+sign_str+"long int"+d; } else if(width==config.ansi_c.char_width) @@ -304,19 +304,19 @@ std::string expr2ct::convert_rec( else if(width==config.ansi_c.short_int_width) { if(is_signed) - sign_str=""; + sign_str.clear(); return q+sign_str+"short int"+d; } else if(width==config.ansi_c.long_long_int_width) { if(is_signed) - sign_str=""; + sign_str.clear(); return q+sign_str+"long long int"+d; } else if(width==128) { if(is_signed) - sign_str=""; + sign_str.clear(); return q + sign_str + "__int128" + d; } else diff --git a/src/cpp/cpp_name.cpp b/src/cpp/cpp_name.cpp index fe456c0ada9..04e898d6d62 100644 --- a/src/cpp/cpp_name.cpp +++ b/src/cpp/cpp_name.cpp @@ -66,7 +66,7 @@ void cpp_namet::convert( identifier+=name_component; if(id=="::") - base_name=""; + base_name.clear(); else base_name+=name_component; } diff --git a/src/cpp/cpp_token.h b/src/cpp/cpp_token.h index 800ac372353..dde77221e5c 100644 --- a/src/cpp/cpp_token.h +++ b/src/cpp/cpp_token.h @@ -29,9 +29,9 @@ class cpp_tokent { kind=0; data.clear(); - text=""; + text.clear(); line_no=0; - filename=""; + filename.clear(); } void swap(cpp_tokent &token) diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 6f28e666b83..eb2d5d69409 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -1270,7 +1270,7 @@ void cpp_typecheck_resolvet::show_identifiers( else if(id_expr.id() == ID_pod_constructor) { out << "constructor "; - id=""; + id.clear(); } else if(id_expr.id()==ID_template_function_instance) { diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp index 09d6f563320..234be8dee16 100644 --- a/src/goto-cc/armcc_mode.cpp +++ b/src/goto-cc/armcc_mode.cpp @@ -129,7 +129,7 @@ int armcc_modet::doit() } else { - compiler.output_file_object=""; + compiler.output_file_object.clear(); compiler.output_file_executable="a.out"; } diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp index fbfc56c6128..64267ea76eb 100644 --- a/src/goto-cc/cw_mode.cpp +++ b/src/goto-cc/cw_mode.cpp @@ -94,7 +94,7 @@ int cw_modet::doit() } else { - compiler.output_file_object=""; + compiler.output_file_object.clear(); compiler.output_file_executable="a.out"; } diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 966821914e6..893c680afef 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -659,7 +659,7 @@ int gcc_modet::doit() } else { - compiler.output_file_object=""; + compiler.output_file_object.clear(); compiler.output_file_executable="a.out"; } @@ -721,14 +721,14 @@ int gcc_modet::doit() { language=arg_it->arg; if(language=="none") - language=""; + language.clear(); } } else if(has_prefix(arg_it->arg, "-x")) { language=std::string(arg_it->arg, 2, std::string::npos); if(language=="none") - language=""; + language.clear(); } } } diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp index e00a6746436..299f110a228 100644 --- a/src/goto-cc/ld_mode.cpp +++ b/src/goto-cc/ld_mode.cpp @@ -123,7 +123,7 @@ int ld_modet::doit() } else { - compiler.output_file_object = ""; + compiler.output_file_object.clear(); compiler.output_file_executable = "a.out"; } diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index 651d3870d3e..d9e4a2fb41c 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/src/goto-cc/ms_cl_cmdline.cpp @@ -438,7 +438,7 @@ void ms_cl_cmdlinet::process_cl_option(const std::string &s) if(s.size()==2) { option.islong=false; - option.optstring=""; + option.optstring.clear(); option.optchar=s[1]; optnr=getoptnr(option.optchar); } @@ -474,7 +474,7 @@ void ms_cl_cmdlinet::process_cl_option(const std::string &s) if(ms_cl_prefix.size()==1) { option.islong=false; - option.optstring=""; + option.optstring.clear(); option.optchar=ms_cl_prefix[0]; optnr=getoptnr(option.optchar); } diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index b89091c33a9..3c76e6d50b7 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -454,7 +454,7 @@ void dump_ct::convert_compound( if(comp_type.id()==ID_c_bit_field && to_c_bit_field_type(comp_type).get_width()==0) { - comp_name=""; + comp_name.clear(); s=type_to_string(comp_type); } @@ -504,7 +504,7 @@ void dump_ct::convert_compound( typedef_map.insert({typedef_str, typedef_infot(typedef_str)}); PRECONDITION(!td_map_entry.second); if(!td_map_entry.first->second.early) - td_map_entry.first->second.type_decl_str=""; + td_map_entry.first->second.type_decl_str.clear(); os << "typedef "; } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 1846ad032e5..7451368f2ff 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -139,12 +139,12 @@ void value_sett::output(const namespacet &ns, std::ostream &out) const if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) { display_name = id2string(e.identifier) + e.suffix; - identifier = ""; + identifier.clear(); } else if(e.identifier == "value_set::return_value") { display_name = "RETURN_VALUE" + e.suffix; - identifier = ""; + identifier.clear(); } else { diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index ca6ee909382..164ecf1e234 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -57,7 +57,7 @@ void value_set_fit::output( if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) { display_name=id2string(e.identifier)+e.suffix; - identifier=""; + identifier.clear(); } else { diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp index 3fddac8cd87..a0b3fe83edd 100644 --- a/src/util/cmdline.cpp +++ b/src/util/cmdline.cpp @@ -169,7 +169,7 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring) option.islong=true; option.optchar=0; option.isset=false; - option.optstring=""; + option.optstring.clear(); for(optstring++; optstring[0]!=')' && optstring[0]!=0; optstring++) option.optstring+=optstring[0]; @@ -181,7 +181,7 @@ bool cmdlinet::parse(int argc, const char **argv, const char *optstring) { option.islong=false; option.optchar=optstring[0]; - option.optstring=""; + option.optstring.clear(); option.isset=false; optstring++; diff --git a/src/util/identifier.cpp b/src/util/identifier.cpp index daa41cad07d..60c8f8cffea 100644 --- a/src/util/identifier.cpp +++ b/src/util/identifier.cpp @@ -43,6 +43,6 @@ void identifiert::parse(const std::string &s) } components.push_back(component); - component=""; + component.clear(); } } diff --git a/src/util/lispexpr.cpp b/src/util/lispexpr.cpp index 94028702844..08f3ed29520 100644 --- a/src/util/lispexpr.cpp +++ b/src/util/lispexpr.cpp @@ -62,7 +62,7 @@ bool lispexprt::parse( std::string::size_type &ptr) { clear(); - value=""; + value.clear(); if(ptr==std::string::npos || ptr>=s.size()) return true; @@ -156,7 +156,7 @@ int test_lispexpr() while(true) { - line=""; + line.clear(); while(true) { diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp index 890396ffc2d..63b3cca5baa 100644 --- a/src/util/lispirep.cpp +++ b/src/util/lispirep.cpp @@ -43,7 +43,7 @@ void lisp2irep(const lispexprt &src, irept &dest) void irep2lisp(const irept &src, lispexprt &dest) { dest.clear(); - dest.value=""; + dest.value.clear(); dest.type=lispexprt::List; #ifdef NAMED_SUB_IS_FORWARD_LIST @@ -65,7 +65,7 @@ void irep2lisp(const irept &src, lispexprt &dest) { lispexprt name; name.type=lispexprt::String; - name.value=""; + name.value.clear(); dest.push_back(name); lispexprt sub; From 29a9ce80eeacce29dedb6f440d1b7ec7b24a51a9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 21:16:49 +0000 Subject: [PATCH 8/9] Remove unnecessary uses of "" Appending "" to a string has no effect. --- src/ansi-c/expr2c.cpp | 4 +--- src/cpp/parse.cpp | 5 ++--- src/goto-instrument/dot.cpp | 10 +++++----- src/goto-programs/property_checker.cpp | 2 +- src/goto-symex/partial_order_concurrency.cpp | 2 -- src/pointer-analysis/value_set.cpp | 2 +- src/pointer-analysis/value_set_fi.cpp | 2 +- src/pointer-analysis/value_set_fivr.cpp | 2 +- src/pointer-analysis/value_set_fivrns.cpp | 2 +- src/solvers/smt2/smt2_conv.cpp | 1 - .../string_constraint_generator_format.cpp | 8 +++++--- src/util/cmdline.cpp | 18 ++++-------------- 12 files changed, 22 insertions(+), 36 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index efc07cc8dd5..b26ce493b11 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -479,9 +479,7 @@ std::string expr2ct::convert_rec( if(parameters.empty()) { - if(code_type.has_ellipsis()) - dest+=""; // empty! - else + if(!code_type.has_ellipsis()) dest+="void"; // means 'no parameters' } else diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 7de7d52e1ae..e1c5da7b7ce 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -839,9 +839,8 @@ bool Parser::rNamespaceSpec(cpp_namespace_spect &namespace_spec) irep_idt name; - if(lex.LookAhead(0)=='{') - name=""; // an anonymous namespace - else + // namespace might be anonymous + if(lex.LookAhead(0) != '{') { if(lex.get_token(tk2)==TOK_IDENTIFIER) name=tk2.data.get(ID_C_base_name); diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index 3c179705674..7dbc7177be4 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -192,12 +192,12 @@ void dott::write_dot_subgraph( std::set fres; find_next(instructions, it, tres, fres); - std::string tlabel="true"; - std::string flabel="false"; - if(fres.empty() || tres.empty()) + std::string tlabel; + std::string flabel; + if(!fres.empty() && !tres.empty()) { - tlabel=""; - flabel=""; + tlabel = "true"; + flabel = "false"; } typedef std::set t; diff --git a/src/goto-programs/property_checker.cpp b/src/goto-programs/property_checker.cpp index 951b8a99289..11ff035bb22 100644 --- a/src/goto-programs/property_checker.cpp +++ b/src/goto-programs/property_checker.cpp @@ -21,7 +21,7 @@ std::string property_checkert::as_string(resultt result) case property_checkert::resultt::UNKNOWN: return "UNKNOWN"; } - return ""; + UNREACHABLE; } property_checkert::property_checkert( diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index 226e504c314..459bd5f8d21 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -133,8 +133,6 @@ irep_idt partial_order_concurrencyt::rw_clock_id( return id2string(id(event))+"$rclk$"+std::to_string(axiom); else UNREACHABLE; - - return ""; } symbol_exprt partial_order_concurrencyt::clock( diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 7451368f2ff..dca1ab5b086 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -181,7 +181,7 @@ void value_sett::output(const namespacet &ns, std::ostream &out) const result = "<" + from_expr(ns, identifier, o) + ", "; if(o_it->second) - result += integer2string(*o_it->second) + ""; + result += integer2string(*o_it->second); else result += '*'; diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 164ecf1e234..224059c779f 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -102,7 +102,7 @@ void value_set_fit::output( result="<"+from_expr(ns, identifier, o)+", "; if(o_it->second) - result += integer2string(*o_it->second) + ""; + result += integer2string(*o_it->second); else result+='*'; diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index f38b26c8cc5..cfe874a0caf 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -143,7 +143,7 @@ void value_set_fivrt::output( result+=from_expr(ns, identifier, o)+", "; if(o_it->second) - result += integer2string(*o_it->second) + ""; + result += integer2string(*o_it->second); else result+='*'; diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index c60994f8c28..0ee50e1dfa5 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -134,7 +134,7 @@ void value_set_fivrnst::output_entry( result+=from_expr(ns, identifier, o)+", "; if(o_it->second) - result += integer2string(*o_it->second) + ""; + result += integer2string(*o_it->second); else result+='*'; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 00dc414bda3..e4410942b4d 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -832,7 +832,6 @@ std::string smt2_convt::type2id(const typet &type) const else { UNREACHABLE; - return ""; } } diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp index cb35a53278c..ca49485ee6e 100644 --- a/src/solvers/strings/string_constraint_generator_format.cpp +++ b/src/solvers/strings/string_constraint_generator_format.cpp @@ -79,6 +79,8 @@ class format_specifiert class format_textt { public: + format_textt() = default; + explicit format_textt(std::string _content) : content(_content) { } @@ -106,7 +108,7 @@ class format_elementt TEXT } format_typet; - explicit format_elementt(format_typet _type) : type(_type), fstring("") + explicit format_elementt(format_typet _type) : type(_type) { } @@ -114,7 +116,7 @@ class format_elementt { } - explicit format_elementt(format_specifiert fs) : type(SPECIFIER), fstring("") + explicit format_elementt(format_specifiert fs) : type(SPECIFIER) { fspec.push_back(fs); } @@ -194,7 +196,7 @@ static bool check_format_string(std::string s) static format_specifiert format_specifier_of_match(std::smatch &m) { int index = m[1].str().empty() ? -1 : std::stoi(m[1].str()); - std::string flag = m[2].str().empty() ? "" : m[2].str(); + std::string flag = m[2].str(); int width = m[3].str().empty() ? -1 : std::stoi(m[3].str()); int precision = m[4].str().empty() ? -1 : std::stoi(m[4].str()); std::string tT = m[5].str(); diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp index a0b3fe83edd..9df7b4dafad 100644 --- a/src/util/cmdline.cpp +++ b/src/util/cmdline.cpp @@ -46,13 +46,8 @@ std::string cmdlinet::get_value(char option) const { auto i=getoptnr(option); - if(i.has_value()) - { - if(options[*i].values.empty()) - return ""; - else - return options[*i].values.front(); - } + if(i.has_value() && !options[*i].values.empty()) + return options[*i].values.front(); else return ""; } @@ -96,13 +91,8 @@ std::string cmdlinet::get_value(const char *option) const { auto i=getoptnr(option); - if(i.has_value()) - { - if(options[*i].values.empty()) - return ""; - else - return options[*i].values.front(); - } + if(i.has_value() && !options[*i].values.empty()) + return options[*i].values.front(); else return ""; } From 13b3e4fdeff46be36ffd91aa21caac1eef366d4a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Feb 2019 22:01:31 +0000 Subject: [PATCH 9/9] Use s.empty() or !s.empty() instead of comparison to irep_idt() This avoids constructing an object when we can just use an integer comparison. --- jbmc/src/java_bytecode/java_entry_point.cpp | 2 +- jbmc/src/java_bytecode/java_object_factory.cpp | 8 +++----- src/ansi-c/parser_static.inc | 4 ++-- src/goto-programs/instrument_preconditions.cpp | 3 +-- src/solvers/smt2/smt2_conv.cpp | 2 +- 5 files changed, 8 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index e2757600fcd..52d673674d1 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -542,7 +542,7 @@ main_function_resultt get_main_symbol( irep_idt main_symbol_id = resolve_friendly_method_name( config.main.value(), symbol_table, error_message); - if(main_symbol_id==irep_idt()) + if(main_symbol_id.empty()) { message.error() << "main symbol resolution failed: " << error_message << messaget::eom; diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index ca635b19805..9e2d493a7d6 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -290,7 +290,7 @@ class recursion_set_entryt /// Removes erase_entry (if set) from the controlled set. ~recursion_set_entryt() { - if(erase_entry!=irep_idt()) + if(!erase_entry.empty()) recursion_set.erase(erase_entry); } @@ -303,10 +303,8 @@ class recursion_set_entryt /// \return true if added to the set (and therefore owned by this object) bool insert_entry(const irep_idt &entry) { - INVARIANT( - erase_entry==irep_idt(), - "insert_entry should only be called once"); - INVARIANT(entry!=irep_idt(), "entry should be a struct tag"); + INVARIANT(erase_entry.empty(), "insert_entry should only be called once"); + INVARIANT(!entry.empty(), "entry should be a struct tag"); bool ret=recursion_set.insert(entry).second; if(ret) { diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 3dc0f024e03..f749027ac66 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -224,7 +224,7 @@ static void make_subtype(typet &dest, typet &src) } else if(p->is_nil()) assert(false); - else if(p->id()==irep_idt()) + else if(p->id().empty()) assert(false); else { @@ -247,7 +247,7 @@ static void make_subtype(typet &dest, typet &src) auto &merged_type = to_merged_type(*p); p=&merged_type.last_type(); } - else if(p->id()==irep_idt()) + else if(p->id().empty()) assert(false); else if(p->is_nil()) assert(false); diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index a5066d298b1..eedb7f55792 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -75,8 +75,7 @@ replace_symbolt actuals_replace_map( std::size_t count=0; for(const auto &p : parameters) { - if(p.get_identifier()!=irep_idt() && - arguments.size()>count) + if(!p.get_identifier().empty() && arguments.size() > count) { const exprt a = typecast_exprt::conditional_cast(arguments[count], p.type()); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e4410942b4d..83f6bf24c27 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -317,7 +317,7 @@ constant_exprt smt2_convt::parse_literal( mp_integer value; - if(src.id()!=irep_idt()) + if(!src.id().empty()) { const std::string &s=src.id_string();