From 57470326ab0bd7e1cd12c6e01919e7c13f51564d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 30 Dec 2023 21:36:54 +0000 Subject: [PATCH] use dstringt::starts_with This replaces has_prefix(id2string(x), y) by x.has_prefix(y). --- .../java_bytecode/java_bytecode_language.cpp | 23 ++++++++----------- .../src/java_bytecode/java_object_factory.cpp | 3 +-- jbmc/src/java_bytecode/java_types.cpp | 12 +++++----- jbmc/src/java_bytecode/java_utils.cpp | 5 ++-- src/ansi-c/c_preprocess.cpp | 6 ++--- src/ansi-c/c_typecheck_expr.cpp | 10 ++++---- src/ansi-c/c_typecheck_initializer.cpp | 3 +-- src/ansi-c/expr2c.cpp | 8 +++---- src/ansi-c/goto_check_c.cpp | 3 +-- src/cpp/cpp_typecheck_resolve.cpp | 7 +++--- src/cprover/axioms.cpp | 9 ++++---- src/cprover/instrument_contracts.cpp | 6 ++--- src/cprover/may_alias.cpp | 11 ++++----- src/cprover/simplify_state_expr.cpp | 9 ++++---- src/goto-cc/compile.cpp | 5 ++-- src/goto-harness/recursive_initialization.cpp | 2 +- src/goto-instrument/branch.cpp | 3 +-- src/goto-instrument/count_eloc.cpp | 2 +- src/goto-instrument/cover_filter.cpp | 2 +- src/goto-instrument/function.cpp | 5 ++-- src/goto-instrument/goto_program2code.cpp | 14 +++++------ src/goto-instrument/nondet_static.cpp | 5 ++-- src/goto-instrument/race_check.cpp | 7 +++--- src/goto-instrument/wmm/shared_buffers.cpp | 14 +++++------ src/goto-instrument/wmm/shared_buffers.h | 3 +-- src/goto-programs/builtin_functions.cpp | 10 ++++---- src/goto-programs/goto_convert.cpp | 5 ++-- src/goto-programs/goto_convert_functions.cpp | 3 +-- src/goto-programs/graphml_witness.cpp | 6 ++--- .../remove_virtual_functions.cpp | 12 ++++------ .../show_goto_functions_json.cpp | 16 ++++++------- src/goto-programs/show_goto_functions_xml.cpp | 14 +++++------ src/goto-programs/slice_global_inits.cpp | 10 ++++---- src/goto-symex/auto_objects.cpp | 3 +-- src/goto-symex/shadow_memory.cpp | 11 ++++----- src/goto-synthesizer/cegis_verifier.cpp | 3 +-- src/linking/static_lifetime_init.cpp | 2 +- src/pointer-analysis/value_set.cpp | 8 +++---- src/pointer-analysis/value_set_fi.cpp | 23 ++++++++----------- .../smt2_incremental/object_tracking.cpp | 4 +--- src/util/format_expr.cpp | 4 +--- src/util/simplify_expr_pointer.cpp | 3 +-- 42 files changed, 135 insertions(+), 179 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 32d870c0494..c01b67e100a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -6,12 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "java_bytecode_language.h" - -#include -#include - -#include +#include "java_bytecode_convert_class.h" #include #include @@ -19,21 +14,22 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include -#include - #include +#include +#include + #include "ci_lazy_methods.h" #include "create_array_with_type_intrinsic.h" +#include "expr2java.h" #include "java_bytecode_concurrency_instrumentation.h" -#include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_instrument.h" #include "java_bytecode_internal_additions.h" +#include "java_bytecode_language.h" #include "java_bytecode_typecheck.h" #include "java_class_loader.h" #include "java_class_loader_limit.h" @@ -44,10 +40,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_utils.h" #include "lambda_synthesis.h" #include "lift_clinit_calls.h" - -#include "expr2java.h" #include "load_method_by_regex.h" +#include +#include + /// Parse options that are java bytecode specific. /// \param cmd: Command line /// \param [out] options: The options object that will be updated. @@ -536,7 +533,7 @@ static symbol_exprt get_or_create_class_literal_symbol( symbolt new_class_symbol{ symbol_expr.get_identifier(), symbol_expr.type(), ID_java}; INVARIANT( - has_prefix(id2string(new_class_symbol.name), "java::"), + new_class_symbol.name.starts_with("java::"), "class identifier should have 'java::' prefix"); new_class_symbol.base_name = id2string(new_class_symbol.name).substr(6); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index b824caefcbc..9236637d0f8 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -204,7 +203,7 @@ void java_object_factoryt::gen_pointer_target_init( PRECONDITION(followed_target_type.id() == ID_struct); const auto &target_class_type = to_java_class_type(followed_target_type); - if(has_prefix(id2string(target_class_type.get_tag()), "java::array[")) + if(target_class_type.get_tag().starts_with("java::array[")) { assignments.append(gen_nondet_array_init( expr, diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index b5d7557a204..d6f2c1b9ffe 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -6,18 +6,18 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include +#include "java_types.h" -#include #include -#include #include #include +#include -#include "java_types.h" #include "java_utils.h" +#include +#include + #ifdef DEBUG #include #endif @@ -232,7 +232,7 @@ exprt get_array_element_type_field(const exprt &pointer) /// of java::array[ bool is_java_array_tag(const irep_idt& tag) { - return has_prefix(id2string(tag), "java::array["); + return tag.starts_with("java::array["); } /// Constructs a type indicated by the given character: diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index dcd5cc86849..a851c2f27f6 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -206,7 +206,7 @@ void merge_source_location_rec( bool is_java_string_literal_id(const irep_idt &id) { - return has_prefix(id2string(id), JAVA_STRING_LITERAL_PREFIX); + return id.starts_with(JAVA_STRING_LITERAL_PREFIX); } irep_idt resolve_friendly_method_name( @@ -221,8 +221,7 @@ irep_idt resolve_friendly_method_name( std::set matches; for(const auto &s : symbol_table.symbols) - if(has_prefix(id2string(s.first), prefix) && - s.second.type.id()==ID_code) + if(s.first.starts_with(prefix) && s.second.type.id() == ID_code) matches.insert(s.first); if(matches.empty()) diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index c753a0b0c31..afe51b01010 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -459,7 +459,7 @@ bool c_preprocess_gcc_clang( { if(arch == "i386" || arch == "x86_64" || arch == "x32") argv.push_back("-m16"); - else if(has_prefix(id2string(arch), "mips")) + else if(arch.starts_with("mips")) argv.push_back("-mips16"); } else if(config.ansi_c.pointer_width == 32) @@ -468,7 +468,7 @@ bool c_preprocess_gcc_clang( argv.push_back("-m32"); else if(arch == "x32") argv.push_back("-mx32"); - else if(has_prefix(id2string(arch), "mips")) + else if(arch.starts_with("mips")) argv.push_back("-mabi=32"); else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le") argv.push_back("-m32"); @@ -481,7 +481,7 @@ bool c_preprocess_gcc_clang( { if(arch == "i386" || arch == "x86_64" || arch == "x32") argv.push_back("-m64"); - else if(has_prefix(id2string(arch), "mips")) + else if(arch.starts_with("mips")) argv.push_back("-mabi=64"); else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le") argv.push_back("-m64"); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 4c8cb1024df..ab278de784f 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -870,7 +869,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) // preserve location expr.add_source_location()=source_location; } - else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity")) + else if(identifier.starts_with(CPROVER_PREFIX "constant_infinity")) { expr=infinity_exprt(symbol.type); @@ -1934,7 +1933,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) throw 0; } } - else if(has_prefix(id2string(statement), "assign")) + else if(statement.starts_with("assign")) typecheck_side_effect_assignment(expr); else if(statement==ID_function_call) typecheck_side_effect_function_call( @@ -3456,9 +3455,8 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); - count_leading_zeros_exprt clz{expr.arguments().front(), - has_prefix(id2string(identifier), "__lzcnt"), - expr.type()}; + count_leading_zeros_exprt clz{ + expr.arguments().front(), identifier.starts_with("__lzcnt"), expr.type()}; clz.add_source_location() = source_location; return std::move(clz); diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 8ff429910db..6dd7934f023 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -231,7 +230,7 @@ exprt c_typecheck_baset::do_initializer_rec( void c_typecheck_baset::do_initializer(symbolt &symbol) { // this one doesn't need initialization - if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity")) + if(symbol.name.starts_with(CPROVER_PREFIX "constant_infinity")) return; if(symbol.is_type) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 8643386266e..6ca3038e1a9 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1650,7 +1650,7 @@ std::string expr2ct::convert_symbol(const exprt &src) dest=id2string(entry->second); #if 0 - if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "::dynamic_object")) + if(id.starts_with(SYMEX_DYNAMIC_PREFIX "::dynamic_object")) { if(sizeof_nesting++ == 0) dest+=" /*"+convert(src.type()); @@ -1992,7 +1992,7 @@ std::string expr2ct::convert_constant( dest="(("+convert(type)+")"+dest+")"; } else if( - value == "INVALID" || has_prefix(id2string(value), "INVALID-") || + value == "INVALID" || value.starts_with("INVALID-") || value == "NULL+offset") { dest = id2string(value); @@ -3729,10 +3729,10 @@ std::string expr2ct::convert_with_precedence( "__builtin_bswap" + integer2string(*pointer_offset_bits( to_unary_expr(src).op().type(), ns))); - else if(has_prefix(src.id_string(), "byte_extract")) + else if(src.id().starts_with("byte_extract")) return convert_byte_extract(to_byte_extract_expr(src), precedence = 16); - else if(has_prefix(src.id_string(), "byte_update")) + else if(src.id().starts_with("byte_update")) return convert_byte_update(to_byte_update_expr(src), precedence = 16); else if(src.id()==ID_address_of) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index b21b76af1ea..992d9af33e7 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -28,7 +28,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -1443,7 +1442,7 @@ void goto_check_ct::pointer_primitive_check( { const auto &symbol_expr = to_symbol_expr(pointer); - if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX)) + if(symbol_expr.get_identifier().starts_with(CPROVER_PREFIX)) return; } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 59f65541ff3..9c46f74d81f 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -15,12 +15,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #endif -#include - #include #include #include -#include #include #include #include @@ -34,6 +31,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_typecheck_fargs.h" #include "cpp_util.h" +#include + cpp_typecheck_resolvet::cpp_typecheck_resolvet(cpp_typecheckt &_cpp_typecheck): cpp_typecheck(_cpp_typecheck), original_scope(nullptr) // set in resolve_scope() @@ -814,7 +813,7 @@ exprt cpp_typecheck_resolvet::do_builtin( dest=type_exprt(typet(base_name)); } - else if(has_prefix(id2string(base_name), "constant_infinity")) + else if(base_name.starts_with("constant_infinity")) { // ok, but type missing dest=exprt(ID_infinity, size_type()); diff --git a/src/cprover/axioms.cpp b/src/cprover/axioms.cpp index 37c0a275be6..6b002370ebc 100644 --- a/src/cprover/axioms.cpp +++ b/src/cprover/axioms.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include @@ -169,13 +168,13 @@ void axiomst::writeable_object() { if(a_it->object_identifier() == "return_value") continue; - else if(has_prefix(id2string(a_it->object_identifier()), "va_args::")) + else if(a_it->object_identifier().starts_with("va_args::")) continue; - else if(has_prefix(id2string(a_it->object_identifier()), "va_arg::")) + else if(a_it->object_identifier().starts_with("va_arg::")) continue; - else if(has_prefix(id2string(a_it->object_identifier()), "va_arg_array::")) + else if(a_it->object_identifier().starts_with("va_arg_array::")) continue; - else if(has_prefix(id2string(a_it->object_identifier()), "old::")) + else if(a_it->object_identifier().starts_with("old::")) continue; auto &symbol = ns.lookup(a_it->object_expr()); diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp index b68b49681dd..88dc0f22ef0 100644 --- a/src/cprover/instrument_contracts.cpp +++ b/src/cprover/instrument_contracts.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include @@ -191,8 +190,7 @@ is_procedure_local(const irep_idt &function_identifier, const exprt &lhs) else if(lhs.id() == ID_symbol) { const auto &symbol_expr = to_symbol_expr(lhs); - return has_prefix( - id2string(symbol_expr.get_identifier()), + return symbol_expr.get_identifier().starts_with( id2string(function_identifier) + "::"); } else @@ -204,7 +202,7 @@ static bool is_old(const exprt &lhs) if(lhs.id() == ID_symbol) { const auto &symbol_expr = to_symbol_expr(lhs); - return has_prefix(id2string(symbol_expr.get_identifier()), "old::"); + return symbol_expr.get_identifier().starts_with("old::"); } else return false; diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp index b3cc69fb84d..046fbbcd84c 100644 --- a/src/cprover/may_alias.cpp +++ b/src/cprover/may_alias.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include @@ -115,15 +114,15 @@ bool stack_and_not_dirty( { auto symbol_expr = object->object_expr(); auto identifier = symbol_expr.get_identifier(); - if(has_prefix(id2string(identifier), "va_arg::")) + if(identifier.starts_with("va_arg::")) return true; // on the stack, and might alias - else if(has_prefix(id2string(identifier), "var_args::")) + else if(identifier.starts_with("var_args::")) return false; // on the stack -- can take address? - else if(has_prefix(id2string(identifier), "va_args::")) + else if(identifier.starts_with("va_args::")) return false; // on the stack -- can take address? - else if(has_prefix(id2string(identifier), "va_arg_array::")) + else if(identifier.starts_with("va_arg_array::")) return false; // on the stack -- can take address? - else if(has_prefix(id2string(identifier), "old::")) + else if(identifier.starts_with("old::")) return true; // on the stack, but can't take address else if(identifier == "return_value") return true; // on the stack, but can't take address diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp index 68b65f4afe3..44700528df2 100644 --- a/src/cprover/simplify_state_expr.cpp +++ b/src/cprover/simplify_state_expr.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include #include @@ -320,14 +319,14 @@ exprt simplify_live_object_expr( { auto identifier = to_object_address_expr(object).object_identifier(); - if(has_prefix(id2string(identifier), "allocate-")) + if(identifier.starts_with("allocate-")) { } else if(identifier == "return_value") { return true_exprt(); // never dies } - else if(has_prefix(id2string(identifier), "va_args::")) + else if(identifier.starts_with("va_args::")) { return true_exprt(); // might be 'dead' } @@ -435,10 +434,10 @@ exprt simplify_writeable_object_expr( { auto identifier = to_object_address_expr(object).object_identifier(); - if(has_prefix(id2string(identifier), "allocate-")) + if(identifier.starts_with("allocate-")) { } - else if(has_prefix(id2string(identifier), "va_args::")) + else if(identifier.starts_with("va_args::")) { return true_exprt(); // always writeable } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 25119867bb7..8eec5b937ae 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -16,7 +16,6 @@ Date: June 2006 #include #include #include -#include #include #include #include @@ -744,10 +743,10 @@ bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table) { const irep_idt &name=pair.second.name; const typet &new_type=pair.second.type; - if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code)) + if(!(name.starts_with(CPROVER_PREFIX) && new_type.id() == ID_code)) continue; - if(has_prefix(id2string(name), FILE_LOCAL_PREFIX)) + if(name.starts_with(FILE_LOCAL_PREFIX)) continue; bool inserted; diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 79bc6bfedc0..fc921934fac 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -1027,7 +1027,7 @@ code_blockt recursive_initializationt::build_function_pointer_constructor( : ""; // skip referencing globals because the corresponding symbols in the symbol // table are no longer marked as file local. - if(has_prefix(id2string(sym_to_lookup), FILE_LOCAL_PREFIX)) + if(sym_to_lookup.starts_with(FILE_LOCAL_PREFIX)) { continue; } diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp index 23670abcd0a..50198aa74c1 100644 --- a/src/goto-instrument/branch.cpp +++ b/src/goto-instrument/branch.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -26,7 +25,7 @@ void branch( for(auto &gf_entry : goto_model.goto_functions.function_map) { // don't instrument our internal functions - if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX)) + if(gf_entry.first.starts_with(CPROVER_PREFIX)) continue; // don't instrument the function to be called, diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index a2185e2f9ab..bdafcfa5608 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -194,7 +194,7 @@ void print_global_state_size(const goto_modelt &goto_model) if( symbol.is_type || symbol.is_macro || symbol.type.id() == ID_code || symbol.type.get_bool(ID_C_constant) || - has_prefix(id2string(symbol.name), CPROVER_PREFIX) || + symbol.name.starts_with(CPROVER_PREFIX) || (has_initialize && initialized.find(symbol.name) == initialized.end())) { continue; diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index 8af94d998f1..1cef763369a 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -34,7 +34,7 @@ bool internal_functions_filtert::operator()( return false; // ignore Java built-ins (synthetic functions) - if(has_prefix(id2string(function.name), "java::array[")) + if(function.name.starts_with("java::array[")) return false; // ignore if built-in library diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 066c2e7edc8..246c0ddec81 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -82,7 +81,7 @@ void function_enter( for(auto &gf_entry : goto_model.goto_functions.function_map) { // don't instrument our internal functions - if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX)) + if(gf_entry.first.starts_with(CPROVER_PREFIX)) continue; // don't instrument the function to be called, @@ -107,7 +106,7 @@ void function_exit( for(auto &gf_entry : goto_model.goto_functions.function_map) { // don't instrument our internal functions - if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX)) + if(gf_entry.first.starts_with(CPROVER_PREFIX)) continue; // don't instrument the function to be called, diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index d69a4bb2fbc..b6e6d2ea725 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -268,8 +268,8 @@ void goto_program2codet::convert_labels( ++it) { if( - has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") || - has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L")) + it->starts_with(CPROVER_PREFIX "ASYNC_") || + it->starts_with(CPROVER_PREFIX "DUMP_L")) { continue; } @@ -1205,8 +1205,8 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto( ++it) { if( - has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_") || - has_prefix(id2string(*it), CPROVER_PREFIX "DUMP_L")) + it->starts_with(CPROVER_PREFIX "ASYNC_") || + it->starts_with(CPROVER_PREFIX "DUMP_L")) { continue; } @@ -1270,7 +1270,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( it=target->labels.begin(); it!=target->labels.end(); ++it) - if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_")) + if(it->starts_with(CPROVER_PREFIX "ASYNC_")) { labels_in_use.insert(*it); @@ -1343,7 +1343,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( it=target->labels.begin(); it!=target->labels.end(); ++it) - if(has_prefix(id2string(*it), CPROVER_PREFIX "ASYNC_")) + if(it->starts_with(CPROVER_PREFIX "ASYNC_")) { labels_in_use.insert(*it); @@ -1862,7 +1862,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) { if(it->second.type.id()!=ID_code) continue; - if(!has_prefix(id2string(it->second.base_name), "nondet_")) + if(!it->second.base_name.starts_with("nondet_")) continue; const code_typet &code_type=to_code_type(it->second.type); if(code_type.return_type() != expr.type()) diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 036b45e4b07..e968a346dba 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -40,7 +40,7 @@ bool is_nondet_initializable_static( const irep_idt &id = symbol_expr.get_identifier(); // is it a __CPROVER_* variable? - if(has_prefix(id2string(id), CPROVER_PREFIX)) + if(id.starts_with(CPROVER_PREFIX)) return false; // variable not in symbol table such as symex variable? @@ -111,8 +111,7 @@ static void nondet_static( const symbol_exprt &fsym = to_symbol_expr(instruction.call_function()); // see cpp/cpp_typecheck.cpp, which creates initialization functions - if(has_prefix( - id2string(fsym.get_identifier()), "#cpp_dynamic_initialization#")) + if(fsym.get_identifier().starts_with("#cpp_dynamic_initialization#")) { nondet_static(ns, goto_functions, fsym.get_identifier()); } diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 7dccfe38fed..fce1b27d0ed 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -13,12 +13,11 @@ Date: February 2006 #include "race_check.h" -#include +#include #include #include -#include #include "rw_set.h" @@ -128,8 +127,8 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" || identifier == "stdout" || identifier == "stderr" || identifier == "sys_nerr" || - has_prefix(id2string(identifier), "symex::invalid_object") || - has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::dynamic_object")) + identifier.starts_with("symex::invalid_object") || + identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::dynamic_object")) return false; // no race check const symbolt &symbol=ns.lookup(identifier); diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 4d73b57efd2..b4140f288fd 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -939,14 +939,12 @@ bool shared_bufferst::is_buffered( { const irep_idt &identifier=symbol_expr.get_identifier(); - if(identifier==CPROVER_PREFIX "alloc" || - identifier==CPROVER_PREFIX "alloc_size" || - identifier=="stdin" || - identifier=="stdout" || - identifier=="stderr" || - identifier=="sys_nerr" || - has_prefix(id2string(identifier), "__unbuffered_") || - has_prefix(id2string(identifier), "__CPROVER")) + if( + identifier == CPROVER_PREFIX "alloc" || + identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" || + identifier == "stdout" || identifier == "stderr" || + identifier == "sys_nerr" || identifier.starts_with("__unbuffered_") || + identifier.starts_with("__CPROVER")) return false; // not buffered const symbolt &symbol=ns.lookup(identifier); diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index b9e6fadb21c..729892b7700 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -154,7 +153,7 @@ class shared_bufferst const symbolt &symbol=ns.lookup(id); if(symbol.is_thread_local) return false; - if(has_prefix(id2string(id), CPROVER_PREFIX)) + if(id.starts_with(CPROVER_PREFIX)) return false; return true; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 8c4df9a84b5..50e49709a93 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -1066,12 +1065,13 @@ void goto_convertt::do_function_call_symbol( { do_prob_coin(lhs, function, arguments, dest); } - else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_")) + else if(identifier.starts_with(CPROVER_PREFIX "prob_uniform_")) { do_prob_uniform(lhs, function, arguments, dest); } - else if(has_prefix(id2string(identifier), "nondet_") || - has_prefix(id2string(identifier), "__VERIFIER_nondet_")) + else if( + identifier.starts_with("nondet_") || + identifier.starts_with("__VERIFIER_nondet_")) { // make it a side effect if there is an LHS if(lhs.is_nil()) @@ -1097,7 +1097,7 @@ void goto_convertt::do_function_call_symbol( assignment.add_source_location()=function.source_location(); copy(assignment, ASSIGN, dest); } - else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_")) + else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) { // make it a side effect if there is an LHS if(lhs.is_nil()) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 7f6adce76cc..bb1289454dd 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com /// Program Transformation #include "goto_convert.h" +#include "goto_convert_class.h" #include #include @@ -18,13 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include #include -#include "goto_convert_class.h" #include "destructor.h" #include "remove_skip.h" @@ -462,7 +461,7 @@ void goto_convertt::convert_label( // magic thread creation label. // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions // that can be executed in parallel, i.e, a new thread. - if(has_prefix(id2string(label), CPROVER_PREFIX "ASYNC_")) + if(label.starts_with(CPROVER_PREFIX "ASYNC_")) { // the body of the thread is expected to be // in the operand. diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 41727b37aac..6370dbd9ad7 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -10,7 +10,6 @@ Date: June 2003 #include "goto_convert_functions.h" -#include #include #include @@ -211,7 +210,7 @@ void goto_convert_functionst::convert_function( // handle SV-COMP's __VERIFIER_atomic_ if( !f.body.instructions.empty() && - has_prefix(id2string(identifier), "__VERIFIER_atomic_")) + identifier.starts_with("__VERIFIER_atomic_")) { goto_programt::instructiont a_begin = goto_programt::make_atomic_begin( f.body.instructions.front().source_location()); diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 60495c65374..50aa2e3bcb2 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -146,7 +146,7 @@ std::string graphml_witnesst::convert_assign_rec( if( comp.get_is_padding() || // for some reason #is_padding gets lost in *some* cases - has_prefix(id2string(comp.get_name()), "$pad")) + comp.get_name().starts_with("$pad")) continue; INVARIANT( @@ -251,7 +251,7 @@ static bool filter_out( // Do not filter out assertions in functions the name of which starts with // CPROVER_PREFIX, because we need to maintain those as violation nodes: // these are assertions generated, for examples, for memory leaks. - if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert()) + if(!id.starts_with(CPROVER_PREFIX) || !it->is_assert()) return true; } @@ -262,7 +262,7 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) { if( expr.id() == ID_symbol && - has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix)) + to_symbol_expr(expr).get_identifier().starts_with(prefix)) { return true; } diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 08eb51fe640..21d96041a1e 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -10,13 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com /// Remove Virtual Function (Method) Calls #include "remove_virtual_functions.h" -#include - #include #include #include #include -#include #include "class_hierarchy.h" #include "class_identifier.h" @@ -24,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "remove_skip.h" #include "resolve_inherited_component.h" +#include + class get_virtual_calleest { public: @@ -524,8 +523,7 @@ void get_virtual_calleest::get_child_functions_rec( if( it != entry_map.end() && (!it->second.symbol_expr.has_value() || - !has_prefix( - id2string(it->second.symbol_expr->get_identifier()), + !it->second.symbol_expr->get_identifier().starts_with( "java::java.lang.Object"))) { continue; @@ -620,9 +618,9 @@ void get_virtual_calleest::get_functions( ? b.symbol_expr->get_identifier() : irep_idt(); - if(has_prefix(id2string(a_id), "java::java.lang.Object")) + if(a_id.starts_with("java::java.lang.Object")) return false; - else if(has_prefix(id2string(b_id), "java::java.lang.Object")) + else if(b_id.starts_with("java::java.lang.Object")) return true; else { diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp index 17f0becb054..eb2b2c8443e 100644 --- a/src/goto-programs/show_goto_functions_json.cpp +++ b/src/goto-programs/show_goto_functions_json.cpp @@ -11,14 +11,13 @@ Author: Thomas Kiley #include "show_goto_functions_json.h" -#include - -#include #include -#include +#include #include "goto_functions.h" +#include + /// For outputting the GOTO program in a readable JSON format. /// \param _list_only: output only list of functions, but not their bodies show_goto_functions_jsont::show_goto_functions_jsont(bool _list_only) @@ -46,11 +45,10 @@ json_objectt show_goto_functions_jsont::convert( json_function["name"] = json_stringt(function_name); json_function["isBodyAvailable"]= jsont::json_boolean(function.body_available()); - bool is_internal= - has_prefix(id2string(function_name), CPROVER_PREFIX) || - has_prefix(id2string(function_name), "java::array[") || - has_prefix(id2string(function_name), "java::org.cprover") || - has_prefix(id2string(function_name), "java::java"); + bool is_internal = function_name.starts_with(CPROVER_PREFIX) || + function_name.starts_with("java::array[") || + function_name.starts_with("java::org.cprover") || + function_name.starts_with("java::java"); json_function["isInternal"]=jsont::json_boolean(is_internal); if(list_only) diff --git a/src/goto-programs/show_goto_functions_xml.cpp b/src/goto-programs/show_goto_functions_xml.cpp index ac4f9c7d3d4..32bc23f9464 100644 --- a/src/goto-programs/show_goto_functions_xml.cpp +++ b/src/goto-programs/show_goto_functions_xml.cpp @@ -11,14 +11,13 @@ Author: Thomas Kiley #include "show_goto_functions_xml.h" -#include - #include -#include #include #include "goto_functions.h" +#include + /// For outputting the GOTO program in a readable xml format. /// \param _list_only: output only list of functions, but not their bodies show_goto_functions_xmlt::show_goto_functions_xmlt(bool _list_only) @@ -50,11 +49,10 @@ xmlt show_goto_functions_xmlt::convert( xml_function.set_attribute("name", id2string(function_name)); xml_function.set_attribute_bool( "is_body_available", function.body_available()); - bool is_internal= - has_prefix(id2string(function_name), CPROVER_PREFIX) || - has_prefix(id2string(function_name), "java::array[") || - has_prefix(id2string(function_name), "java::org.cprover") || - has_prefix(id2string(function_name), "java::java"); + bool is_internal = function_name.starts_with(CPROVER_PREFIX) || + function_name.starts_with("java::array[") || + function_name.starts_with("java::org.cprover") || + function_name.starts_with("java::java"); xml_function.set_attribute_bool("is_internal", is_internal); if(list_only) diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 383ade80a04..05d9287e03c 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -13,13 +13,11 @@ Date: December 2016 #include "slice_global_inits.h" -#include - +#include #include #include -#include -#include +#include #include #include "goto_functions.h" @@ -98,7 +96,7 @@ void slice_global_inits( // if we are to keep the left-hand side, then we also need to keep all // symbols occurring in the right-hand side if( - has_prefix(id2string(id), CPROVER_PREFIX) || + id.starts_with(CPROVER_PREFIX) || symbols_to_keep.find(id) != symbols_to_keep.end()) { fixed_point_reached = false; @@ -122,7 +120,7 @@ void slice_global_inits( if( it->second.is_static_lifetime && !it->second.is_type && !it->second.is_macro && it->second.type.id() != ID_code && - !has_prefix(id2string(it->first), CPROVER_PREFIX) && + !it->first.starts_with(CPROVER_PREFIX) && symbols_to_keep.find(it->first) == symbols_to_keep.end()) { symbolt &symbol = it.get_writeable_symbol(); diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index 3f3321f8b8d..ed5683dbd68 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -84,7 +83,7 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state) { const symbolt &symbol = ns.lookup(obj_identifier); - if(has_prefix(id2string(symbol.base_name), "symex::auto_object")) + if(symbol.base_name.starts_with("symex::auto_object")) { // done already? if(!state.get_level2().current_names.has_key( diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index 1a5ba61d02b..f587f29e39c 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -17,7 +17,6 @@ Author: Peter Schrammel #include #include #include -#include #include #include @@ -352,8 +351,8 @@ void shadow_memoryt::symex_field_static_init( return; if( - has_prefix(id2string(identifier), CPROVER_PREFIX) && - !has_prefix(id2string(identifier), CPROVER_PREFIX "errno")) + identifier.starts_with(CPROVER_PREFIX) && + !identifier.starts_with(CPROVER_PREFIX "errno")) { return; } @@ -383,9 +382,9 @@ void shadow_memoryt::symex_field_static_init_string_constant( { if( expr.get_original_expr().id() == ID_symbol && - has_prefix( - id2string(to_symbol_expr(expr.get_original_expr()).get_identifier()), - CPROVER_PREFIX)) + to_symbol_expr(expr.get_original_expr()) + .get_identifier() + .starts_with(CPROVER_PREFIX)) { return; } diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 57bbfdf30fb..f3a760087dd 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -16,7 +16,6 @@ Author: Qinheping Hu #include #include #include -#include #include #include @@ -45,7 +44,7 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) { if( it->id() == ID_symbol && - has_prefix(id2string(to_symbol_expr(*it).get_identifier()), prefix)) + to_symbol_expr(*it).get_identifier().starts_with(prefix)) { return true; } diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 88432dfbf2d..a8727ffa237 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -44,7 +44,7 @@ static std::optional static_lifetime_init( return {}; // just for linking - if(has_prefix(id2string(identifier), CPROVER_PREFIX "architecture_")) + if(identifier.starts_with(CPROVER_PREFIX "architecture_")) return {}; const typet &type = ns.follow(symbol.type); diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index ca0ef7a0cbb..1108a17e9f9 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -47,9 +47,9 @@ object_numberingt value_sett::object_numbering; bool value_sett::field_sensitive(const irep_idt &id, const typet &type) { // we always track fields on these - if(has_prefix(id2string(id), "value_set::dynamic_object") || - id=="value_set::return_value" || - id=="value_set::memory") + if( + id.starts_with("value_set::dynamic_object") || + id == "value_set::return_value" || id == "value_set::memory") return true; // otherwise it has to be a struct @@ -144,7 +144,7 @@ void value_sett::output(std::ostream &out, const std::string &indent) const values.iterate([&](const irep_idt &, const entryt &e) { irep_idt identifier, display_name; - if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) + if(e.identifier.starts_with("value_set::dynamic_object")) { display_name = id2string(e.identifier) + e.suffix; identifier.clear(); diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 5116999300e..a5fc395b480 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -48,7 +47,7 @@ void value_set_fit::output( const entryt &e=v_it->second; - if(has_prefix(id2string(e.identifier), "value_set::dynamic_object")) + if(e.identifier.starts_with("value_set::dynamic_object")) { display_name=id2string(e.identifier)+e.suffix; identifier.clear(); @@ -253,10 +252,9 @@ bool value_set_fit::make_union(const value_set_fit::valuest &new_values) if(it2==values.end()) { // we always track these - if(has_prefix(id2string(it->second.identifier), - "value_set::dynamic_object") || - has_prefix(id2string(it->second.identifier), - "value_set::return_value")) + if( + it->second.identifier.starts_with("value_set::dynamic_object") || + it->second.identifier.starts_with("value_set::return_value")) { values.insert(*it); result=true; @@ -466,7 +464,7 @@ void value_set_fit::get_value_set_rec( irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix; valuest::const_iterator v_it=values.find(ident); - if(has_prefix(id2string(ident), alloc_adapter_prefix)) + if(ident.starts_with(alloc_adapter_prefix)) { insert(dest, expr, mp_integer{0}); return; @@ -1205,12 +1203,11 @@ void value_set_fit::assign_rec( { const irep_idt &identifier = to_symbol_expr(lhs).get_identifier(); - if(has_prefix(id2string(identifier), - "value_set::dynamic_object") || - has_prefix(id2string(identifier), - "value_set::return_value") || - values.find(id2string(identifier)+suffix)!=values.end()) - // otherwise we don't track this value + if( + identifier.starts_with("value_set::dynamic_object") || + identifier.starts_with("value_set::return_value") || + values.find(id2string(identifier) + suffix) != values.end()) + // otherwise we don't track this value { entryt &entry = get_entry(identifier, suffix); diff --git a/src/solvers/smt2_incremental/object_tracking.cpp b/src/solvers/smt2_incremental/object_tracking.cpp index eda891d985d..e9571d08b1b 100644 --- a/src/solvers/smt2_incremental/object_tracking.cpp +++ b/src/solvers/smt2_incremental/object_tracking.cpp @@ -6,7 +6,6 @@ #include #include #include -#include #include #include #include @@ -93,8 +92,7 @@ static bool is_dynamic(const exprt &object) return true; const auto symbol = expr_try_dynamic_cast(object); bool symbol_is_dynamic = - symbol && - has_prefix(id2string(symbol->get_identifier()), SYMEX_DYNAMIC_PREFIX); + symbol && symbol->get_identifier().starts_with(SYMEX_DYNAMIC_PREFIX); return symbol_is_dynamic; } diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 92cc2e1c099..b7dc5bb8185 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "mathematical_expr.h" #include "mp_arith.h" #include "pointer_expr.h" -#include "prefix.h" #include "string_utils.h" #include @@ -198,8 +197,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src) if(is_null_pointer(src)) return os << ID_NULL; else if( - src.get_value() == "INVALID" || - has_prefix(id2string(src.get_value()), "INVALID-")) + src.get_value() == "INVALID" || src.get_value().starts_with("INVALID-")) { return os << "INVALID-POINTER"; } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 0749edda770..4d496e9abf4 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_expr.h" #include "pointer_offset_size.h" #include "pointer_predicates.h" -#include "prefix.h" #include "std_expr.h" #include "string_constant.h" @@ -600,7 +599,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr) // this is for the benefit of symex return make_boolean_expr( - has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::")); + identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::")); } else if(op_object.id() == ID_string_constant) {