Skip to content

Commit 1ca677b

Browse files
kroeningkroening
committed
use dstringt::starts_with
This replaces has_prefix(id2string(x), y) by x.has_prefix(y).
1 parent 2ab4d2d commit 1ca677b

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+138
-181
lines changed

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -6,34 +6,30 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include "java_bytecode_language.h"
10-
11-
#include <fstream>
12-
#include <string>
13-
14-
#include <linking/static_lifetime_init.h>
9+
#include "java_bytecode_convert_class.h"
1510

1611
#include <util/cmdline.h>
1712
#include <util/config.h>
1813
#include <util/expr_iterator.h>
1914
#include <util/invariant.h>
2015
#include <util/journalling_symbol_table.h>
2116
#include <util/options.h>
22-
#include <util/prefix.h>
2317
#include <util/suffix.h>
2418
#include <util/symbol_table_builder.h>
2519

26-
#include <json/json_parser.h>
27-
2820
#include <goto-programs/class_hierarchy.h>
2921

22+
#include <json/json_parser.h>
23+
#include <linking/static_lifetime_init.h>
24+
3025
#include "ci_lazy_methods.h"
3126
#include "create_array_with_type_intrinsic.h"
27+
#include "expr2java.h"
3228
#include "java_bytecode_concurrency_instrumentation.h"
33-
#include "java_bytecode_convert_class.h"
3429
#include "java_bytecode_convert_method.h"
3530
#include "java_bytecode_instrument.h"
3631
#include "java_bytecode_internal_additions.h"
32+
#include "java_bytecode_language.h"
3733
#include "java_bytecode_typecheck.h"
3834
#include "java_class_loader.h"
3935
#include "java_class_loader_limit.h"
@@ -44,10 +40,11 @@ Author: Daniel Kroening, [email protected]
4440
#include "java_utils.h"
4541
#include "lambda_synthesis.h"
4642
#include "lift_clinit_calls.h"
47-
48-
#include "expr2java.h"
4943
#include "load_method_by_regex.h"
5044

45+
#include <fstream>
46+
#include <string>
47+
5148
/// Parse options that are java bytecode specific.
5249
/// \param cmd: Command line
5350
/// \param [out] options: The options object that will be updated.
@@ -536,7 +533,7 @@ static symbol_exprt get_or_create_class_literal_symbol(
536533
symbolt new_class_symbol{
537534
symbol_expr.get_identifier(), symbol_expr.type(), ID_java};
538535
INVARIANT(
539-
has_prefix(id2string(new_class_symbol.name), "java::"),
536+
new_class_symbol.name.starts_with("java::"),
540537
"class identifier should have 'java::' prefix");
541538
new_class_symbol.base_name =
542539
id2string(new_class_symbol.name).substr(6);

‎jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/interval_constraint.h>
1616
#include <util/message.h>
1717
#include <util/nondet_bool.h>
18-
#include <util/prefix.h>
1918
#include <util/symbol_table_base.h>
2019

2120
#include <goto-programs/class_identifier.h>
@@ -204,7 +203,7 @@ void java_object_factoryt::gen_pointer_target_init(
204203
PRECONDITION(followed_target_type.id() == ID_struct);
205204

206205
const auto &target_class_type = to_java_class_type(followed_target_type);
207-
if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
206+
if(target_class_type.get_tag().starts_with("java::array["))
208207
{
209208
assignments.append(gen_nondet_array_init(
210209
expr,

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,18 +6,18 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <cctype>
10-
#include <iterator>
9+
#include "java_types.h"
1110

12-
#include <util/prefix.h>
1311
#include <util/c_types.h>
14-
#include <util/std_expr.h>
1512
#include <util/ieee_float.h>
1613
#include <util/invariant.h>
14+
#include <util/std_expr.h>
1715

18-
#include "java_types.h"
1916
#include "java_utils.h"
2017

18+
#include <cctype>
19+
#include <iterator>
20+
2121
#ifdef DEBUG
2222
#include <iostream>
2323
#endif
@@ -232,7 +232,7 @@ exprt get_array_element_type_field(const exprt &pointer)
232232
/// of java::array[
233233
bool is_java_array_tag(const irep_idt& tag)
234234
{
235-
return has_prefix(id2string(tag), "java::array[");
235+
return tag.starts_with("java::array[");
236236
}
237237

238238
/// Constructs a type indicated by the given character:

‎jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ void merge_source_location_rec(
206206

207207
bool is_java_string_literal_id(const irep_idt &id)
208208
{
209-
return has_prefix(id2string(id), JAVA_STRING_LITERAL_PREFIX);
209+
return id.starts_with(JAVA_STRING_LITERAL_PREFIX);
210210
}
211211

212212
irep_idt resolve_friendly_method_name(
@@ -221,8 +221,7 @@ irep_idt resolve_friendly_method_name(
221221
std::set<irep_idt> matches;
222222

223223
for(const auto &s : symbol_table.symbols)
224-
if(has_prefix(id2string(s.first), prefix) &&
225-
s.second.type.id()==ID_code)
224+
if(s.first.starts_with(prefix) && s.second.type.id() == ID_code)
226225
matches.insert(s.first);
227226

228227
if(matches.empty())

‎src/ansi-c/c_preprocess.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -459,7 +459,7 @@ bool c_preprocess_gcc_clang(
459459
{
460460
if(arch == "i386" || arch == "x86_64" || arch == "x32")
461461
argv.push_back("-m16");
462-
else if(has_prefix(id2string(arch), "mips"))
462+
else if(arch.starts_with("mips"))
463463
argv.push_back("-mips16");
464464
}
465465
else if(config.ansi_c.pointer_width == 32)
@@ -468,7 +468,7 @@ bool c_preprocess_gcc_clang(
468468
argv.push_back("-m32");
469469
else if(arch == "x32")
470470
argv.push_back("-mx32");
471-
else if(has_prefix(id2string(arch), "mips"))
471+
else if(arch.starts_with("mips"))
472472
argv.push_back("-mabi=32");
473473
else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le")
474474
argv.push_back("-m32");
@@ -481,7 +481,7 @@ bool c_preprocess_gcc_clang(
481481
{
482482
if(arch == "i386" || arch == "x86_64" || arch == "x32")
483483
argv.push_back("-m64");
484-
else if(has_prefix(id2string(arch), "mips"))
484+
else if(arch.starts_with("mips"))
485485
argv.push_back("-mabi=64");
486486
else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le")
487487
argv.push_back("-m64");

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
2222
#include <util/pointer_expr.h>
2323
#include <util/pointer_offset_size.h>
2424
#include <util/pointer_predicates.h>
25-
#include <util/prefix.h>
2625
#include <util/range.h>
2726
#include <util/simplify_expr.h>
2827
#include <util/string_constant.h>
@@ -870,7 +869,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
870869
// preserve location
871870
expr.add_source_location()=source_location;
872871
}
873-
else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity"))
872+
else if(identifier.starts_with(CPROVER_PREFIX "constant_infinity"))
874873
{
875874
expr=infinity_exprt(symbol.type);
876875

@@ -1934,7 +1933,7 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
19341933
throw 0;
19351934
}
19361935
}
1937-
else if(has_prefix(id2string(statement), "assign"))
1936+
else if(statement.starts_with("assign"))
19381937
typecheck_side_effect_assignment(expr);
19391938
else if(statement==ID_function_call)
19401939
typecheck_side_effect_function_call(
@@ -3449,9 +3448,8 @@ exprt c_typecheck_baset::do_special_functions(
34493448

34503449
typecheck_function_call_arguments(expr);
34513450

3452-
count_leading_zeros_exprt clz{expr.arguments().front(),
3453-
has_prefix(id2string(identifier), "__lzcnt"),
3454-
expr.type()};
3451+
count_leading_zeros_exprt clz{
3452+
expr.arguments().front(), identifier.starts_with("__lzcnt"), expr.type()};
34553453
clz.add_source_location() = source_location;
34563454

34573455
return std::move(clz);

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/config.h>
1616
#include <util/cprover_prefix.h>
1717
#include <util/expr_initializer.h>
18-
#include <util/prefix.h>
1918
#include <util/std_types.h>
2019
#include <util/string_constant.h>
2120
#include <util/symbol_table_base.h>
@@ -231,7 +230,7 @@ exprt c_typecheck_baset::do_initializer_rec(
231230
void c_typecheck_baset::do_initializer(symbolt &symbol)
232231
{
233232
// this one doesn't need initialization
234-
if(has_prefix(id2string(symbol.name), CPROVER_PREFIX "constant_infinity"))
233+
if(symbol.name.starts_with(CPROVER_PREFIX "constant_infinity"))
235234
return;
236235

237236
if(symbol.is_type)

‎src/ansi-c/expr2c.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1650,7 +1650,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
16501650
dest=id2string(entry->second);
16511651

16521652
#if 0
1653-
if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
1653+
if(id.starts_with(SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
16541654
{
16551655
if(sizeof_nesting++ == 0)
16561656
dest+=" /*"+convert(src.type());
@@ -1992,7 +1992,7 @@ std::string expr2ct::convert_constant(
19921992
dest="(("+convert(type)+")"+dest+")";
19931993
}
19941994
else if(
1995-
value == "INVALID" || has_prefix(id2string(value), "INVALID-") ||
1995+
value == "INVALID" || value.starts_with("INVALID-") ||
19961996
value == "NULL+offset")
19971997
{
19981998
dest = id2string(value);
@@ -3729,10 +3729,10 @@ std::string expr2ct::convert_with_precedence(
37293729
"__builtin_bswap" + integer2string(*pointer_offset_bits(
37303730
to_unary_expr(src).op().type(), ns)));
37313731

3732-
else if(has_prefix(src.id_string(), "byte_extract"))
3732+
else if(src.id().starts_with("byte_extract"))
37333733
return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
37343734

3735-
else if(has_prefix(src.id_string(), "byte_update"))
3735+
else if(src.id().starts_with("byte_update"))
37363736
return convert_byte_update(to_byte_update_expr(src), precedence = 16);
37373737

37383738
else if(src.id()==ID_address_of)

‎src/ansi-c/goto_check_c.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ Author: Daniel Kroening, [email protected]
2828
#include <util/pointer_expr.h>
2929
#include <util/pointer_offset_size.h>
3030
#include <util/pointer_predicates.h>
31-
#include <util/prefix.h>
3231
#include <util/simplify_expr.h>
3332
#include <util/std_code.h>
3433
#include <util/std_expr.h>
@@ -1443,7 +1442,7 @@ void goto_check_ct::pointer_primitive_check(
14431442
{
14441443
const auto &symbol_expr = to_symbol_expr(pointer);
14451444

1446-
if(has_prefix(id2string(symbol_expr.get_identifier()), CPROVER_PREFIX))
1445+
if(symbol_expr.get_identifier().starts_with(CPROVER_PREFIX))
14471446
return;
14481447
}
14491448

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,9 @@ Author: Daniel Kroening, [email protected]
1515
#include <iostream>
1616
#endif
1717

18-
#include <algorithm>
19-
2018
#include <util/arith_tools.h>
2119
#include <util/c_types.h>
2220
#include <util/mathematical_types.h>
23-
#include <util/prefix.h>
2421
#include <util/simplify_expr.h>
2522
#include <util/std_expr.h>
2623
#include <util/string_constant.h>
@@ -34,6 +31,8 @@ Author: Daniel Kroening, [email protected]
3431
#include "cpp_typecheck_fargs.h"
3532
#include "cpp_util.h"
3633

34+
#include <algorithm>
35+
3736
cpp_typecheck_resolvet::cpp_typecheck_resolvet(cpp_typecheckt &_cpp_typecheck):
3837
cpp_typecheck(_cpp_typecheck),
3938
original_scope(nullptr) // set in resolve_scope()
@@ -814,7 +813,7 @@ exprt cpp_typecheck_resolvet::do_builtin(
814813

815814
dest=type_exprt(typet(base_name));
816815
}
817-
else if(has_prefix(id2string(base_name), "constant_infinity"))
816+
else if(base_name.starts_with("constant_infinity"))
818817
{
819818
// ok, but type missing
820819
dest=exprt(ID_infinity, size_type());

‎src/cprover/axioms.cpp

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/namespace.h>
1818
#include <util/pointer_offset_size.h>
1919
#include <util/pointer_predicates.h>
20-
#include <util/prefix.h>
2120
#include <util/string_constant.h>
2221
#include <util/symbol.h>
2322

@@ -169,13 +168,13 @@ void axiomst::writeable_object()
169168
{
170169
if(a_it->object_identifier() == "return_value")
171170
continue;
172-
else if(has_prefix(id2string(a_it->object_identifier()), "va_args::"))
171+
else if(a_it->object_identifier().starts_with("va_args::"))
173172
continue;
174-
else if(has_prefix(id2string(a_it->object_identifier()), "va_arg::"))
173+
else if(a_it->object_identifier().starts_with("va_arg::"))
175174
continue;
176-
else if(has_prefix(id2string(a_it->object_identifier()), "va_arg_array::"))
175+
else if(a_it->object_identifier().starts_with("va_arg_array::"))
177176
continue;
178-
else if(has_prefix(id2string(a_it->object_identifier()), "old::"))
177+
else if(a_it->object_identifier().starts_with("old::"))
179178
continue;
180179

181180
auto &symbol = ns.lookup(a_it->object_expr());

‎src/cprover/instrument_contracts.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/c_types.h>
1515
#include <util/mathematical_expr.h>
1616
#include <util/pointer_predicates.h>
17-
#include <util/prefix.h>
1817
#include <util/replace_symbol.h>
1918
#include <util/std_code.h>
2019

@@ -191,8 +190,7 @@ is_procedure_local(const irep_idt &function_identifier, const exprt &lhs)
191190
else if(lhs.id() == ID_symbol)
192191
{
193192
const auto &symbol_expr = to_symbol_expr(lhs);
194-
return has_prefix(
195-
id2string(symbol_expr.get_identifier()),
193+
return symbol_expr.get_identifier().starts_with(
196194
id2string(function_identifier) + "::");
197195
}
198196
else
@@ -204,7 +202,7 @@ static bool is_old(const exprt &lhs)
204202
if(lhs.id() == ID_symbol)
205203
{
206204
const auto &symbol_expr = to_symbol_expr(lhs);
207-
return has_prefix(id2string(symbol_expr.get_identifier()), "old::");
205+
return symbol_expr.get_identifier().starts_with("old::");
208206
}
209207
else
210208
return false;

‎src/cprover/may_alias.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/c_types.h>
1515
#include <util/namespace.h>
1616
#include <util/pointer_expr.h>
17-
#include <util/prefix.h>
1817
#include <util/std_expr.h>
1918
#include <util/symbol.h>
2019

@@ -115,15 +114,15 @@ bool stack_and_not_dirty(
115114
{
116115
auto symbol_expr = object->object_expr();
117116
auto identifier = symbol_expr.get_identifier();
118-
if(has_prefix(id2string(identifier), "va_arg::"))
117+
if(identifier.starts_with("va_arg::"))
119118
return true; // on the stack, and might alias
120-
else if(has_prefix(id2string(identifier), "var_args::"))
119+
else if(identifier.starts_with("var_args::"))
121120
return false; // on the stack -- can take address?
122-
else if(has_prefix(id2string(identifier), "va_args::"))
121+
else if(identifier.starts_with("va_args::"))
123122
return false; // on the stack -- can take address?
124-
else if(has_prefix(id2string(identifier), "va_arg_array::"))
123+
else if(identifier.starts_with("va_arg_array::"))
125124
return false; // on the stack -- can take address?
126-
else if(has_prefix(id2string(identifier), "old::"))
125+
else if(identifier.starts_with("old::"))
127126
return true; // on the stack, but can't take address
128127
else if(identifier == "return_value")
129128
return true; // on the stack, but can't take address

0 commit comments

Comments
 (0)