Use dstringt::starts_with

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -6,34 +6,30 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "java_bytecode_language.h"
-
-#include <fstream>
-#include <string>
-
-#include <linking/static_lifetime_init.h>
+#include "java_bytecode_convert_class.h"
 
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/expr_iterator.h>
 #include <util/invariant.h>
 #include <util/journalling_symbol_table.h>
 #include <util/options.h>
-#include <util/prefix.h>
 #include <util/suffix.h>
 #include <util/symbol_table_builder.h>
 
-#include <json/json_parser.h>
-
 #include <goto-programs/class_hierarchy.h>
 
+#include <json/json_parser.h>
+#include <linking/static_lifetime_init.h>
+
 #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, [email protected]
 #include "java_utils.h"
 #include "lambda_synthesis.h"
 #include "lift_clinit_calls.h"
-
-#include "expr2java.h"
 #include "load_method_by_regex.h"
 
+#include <fstream>
+#include <string>
+
 /// 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);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/interval_constraint.h>
 #include <util/message.h>
 #include <util/nondet_bool.h>
-#include <util/prefix.h>
 #include <util/symbol_table_base.h>
 
 #include <goto-programs/class_identifier.h>
@@ -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,

jbmc/src/java_bytecode/java_types.cpp

@@ -6,18 +6,18 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <cctype>
-#include <iterator>
+#include "java_types.h"
 
-#include <util/prefix.h>
 #include <util/c_types.h>
-#include <util/std_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
+#include <util/std_expr.h>
 
-#include "java_types.h"
 #include "java_utils.h"
 
+#include <cctype>
+#include <iterator>
+
 #ifdef DEBUG
 #include <iostream>
 #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:

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<irep_idt> 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())

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");

src/ansi-c/c_typecheck_expr.cpp

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/prefix.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
@@ -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);

src/ansi-c/c_typecheck_initializer.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_initializer.h>
-#include <util/prefix.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 #include <util/symbol_table_base.h>
@@ -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)

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)

src/ansi-c/goto_check_c.cpp

@@ -28,7 +28,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -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;
   }
 

src/cpp/cpp_typecheck_resolve.cpp

@@ -15,12 +15,9 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
-#include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
@@ -34,6 +31,8 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_typecheck_fargs.h"
 #include "cpp_util.h"
 
+#include <algorithm>
+
 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());

src/cprover/axioms.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/prefix.h>
 #include <util/string_constant.h>
 #include <util/symbol.h>
 
@@ -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());

src/cprover/instrument_contracts.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/mathematical_expr.h>
 #include <util/pointer_predicates.h>
-#include <util/prefix.h>
 #include <util/replace_symbol.h>
 #include <util/std_code.h>
 
@@ -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;

src/cprover/may_alias.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
-#include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
@@ -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