Skip to content

Commit 1e0ac30

Browse files
author
Owen Jones
committed
Turn get_may, set_may, etc into irep_ids
1 parent bf7ed1a commit 1e0ac30

File tree

7 files changed

+44
-41
lines changed

7 files changed

+44
-41
lines changed

‎src/analyses/custom_bitvector_analysis.cpp

+19-19
Original file line numberDiff line numberDiff line change
@@ -319,10 +319,11 @@ void custom_bitvector_domaint::transform(
319319
{
320320
const irep_idt &identifier=to_symbol_expr(function).get_identifier();
321321

322-
if(identifier=="__CPROVER_set_must" ||
323-
identifier=="__CPROVER_clear_must" ||
324-
identifier=="__CPROVER_set_may" ||
325-
identifier=="__CPROVER_clear_may")
322+
if(
323+
identifier == CPROVER_PREFIX "set_must" ||
324+
identifier == CPROVER_PREFIX "clear_must" ||
325+
identifier == CPROVER_PREFIX "set_may" ||
326+
identifier == CPROVER_PREFIX "clear_may")
326327
{
327328
if(code_function_call.arguments().size()==2)
328329
{
@@ -331,13 +332,13 @@ void custom_bitvector_domaint::transform(
331332

332333
modet mode;
333334

334-
if(identifier=="__CPROVER_set_must")
335+
if(identifier == CPROVER_PREFIX "set_must")
335336
mode=modet::SET_MUST;
336-
else if(identifier=="__CPROVER_clear_must")
337+
else if(identifier == CPROVER_PREFIX "clear_must")
337338
mode=modet::CLEAR_MUST;
338-
else if(identifier=="__CPROVER_set_may")
339+
else if(identifier == CPROVER_PREFIX "set_may")
339340
mode=modet::SET_MAY;
340-
else if(identifier=="__CPROVER_clear_may")
341+
else if(identifier == CPROVER_PREFIX "clear_may")
341342
mode=modet::CLEAR_MAY;
342343
else
343344
UNREACHABLE;
@@ -459,13 +460,13 @@ void custom_bitvector_domaint::transform(
459460

460461
modet mode;
461462

462-
if(statement=="set_must")
463+
if(statement == ID_set_must)
463464
mode=modet::SET_MUST;
464-
else if(statement=="clear_must")
465+
else if(statement == ID_clear_must)
465466
mode=modet::CLEAR_MUST;
466-
else if(statement=="set_may")
467+
else if(statement == ID_set_may)
467468
mode=modet::SET_MAY;
468-
else if(statement=="clear_may")
469+
else if(statement == ID_clear_may)
469470
mode=modet::CLEAR_MAY;
470471
else
471472
UNREACHABLE;
@@ -664,8 +665,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)
664665

665666
bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
666667
{
667-
if(src.id()=="get_must" ||
668-
src.id()=="get_may")
668+
if(src.id() == ID_get_must || src.id() == ID_get_may)
669669
return true;
670670

671671
forall_operands(it, src)
@@ -679,7 +679,7 @@ exprt custom_bitvector_domaint::eval(
679679
const exprt &src,
680680
custom_bitvector_analysist &custom_bitvector_analysis) const
681681
{
682-
if(src.id()=="get_must" || src.id()=="get_may")
682+
if(src.id() == ID_get_must || src.id() == ID_get_may)
683683
{
684684
if(src.operands().size()==2)
685685
{
@@ -694,15 +694,15 @@ exprt custom_bitvector_domaint::eval(
694694
if(pointer.is_constant() &&
695695
to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
696696
{
697-
if(src.id()=="get_may")
697+
if(src.id() == ID_get_may)
698698
{
699699
for(const auto &bit : may_bits)
700700
if(get_bit(bit.second, bit_nr))
701701
return true_exprt();
702702

703703
return false_exprt();
704704
}
705-
else if(src.id()=="get_must")
705+
else if(src.id() == ID_get_must)
706706
{
707707
return false_exprt();
708708
}
@@ -716,9 +716,9 @@ exprt custom_bitvector_domaint::eval(
716716

717717
bool value=false;
718718

719-
if(src.id()=="get_must")
719+
if(src.id() == ID_get_must)
720720
value=get_bit(v.must_bits, bit_nr);
721-
else if(src.id()=="get_may")
721+
else if(src.id() == ID_get_may)
722722
value=get_bit(v.may_bits, bit_nr);
723723

724724
if(value)

‎src/ansi-c/c_typecheck_expr.cpp

+4-6
Original file line numberDiff line numberDiff line change
@@ -2035,9 +2035,8 @@ exprt c_typecheck_baset::do_special_functions(
20352035

20362036
typecheck_function_call_arguments(expr);
20372037

2038-
exprt get_must_expr=
2039-
binary_predicate_exprt(
2040-
expr.arguments()[0], "get_must", expr.arguments()[1]);
2038+
exprt get_must_expr = binary_predicate_exprt(
2039+
expr.arguments()[0], ID_get_must, expr.arguments()[1]);
20412040
get_must_expr.add_source_location()=source_location;
20422041

20432042
return get_must_expr;
@@ -2053,9 +2052,8 @@ exprt c_typecheck_baset::do_special_functions(
20532052

20542053
typecheck_function_call_arguments(expr);
20552054

2056-
exprt get_may_expr=
2057-
binary_predicate_exprt(
2058-
expr.arguments()[0], "get_may", expr.arguments()[1]);
2055+
exprt get_may_expr = binary_predicate_exprt(
2056+
expr.arguments()[0], ID_get_may, expr.arguments()[1]);
20592057
get_may_expr.add_source_location()=source_location;
20602058

20612059
return get_may_expr;

‎src/ansi-c/expr2c.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -2929,8 +2929,7 @@ std::string expr2ct::convert_code(
29292929
if(statement==ID_array_replace)
29302930
return convert_code_array_replace(src, indent);
29312931

2932-
if(statement=="set_may" ||
2933-
statement=="set_must")
2932+
if(statement == ID_set_may || statement == ID_set_must)
29342933
return
29352934
indent_str(indent)+convert_function(src, id2string(statement), 16)+";";
29362935

@@ -3493,10 +3492,10 @@ std::string expr2ct::convert_with_precedence(
34933492
else if(src.id()==ID_pointer_object)
34943493
return convert_function(src, "POINTER_OBJECT", precedence=16);
34953494

3496-
else if(src.id()=="get_must")
3495+
else if(src.id() == ID_get_must)
34973496
return convert_function(src, "__CPROVER_get_must", precedence=16);
34983497

3499-
else if(src.id()=="get_may")
3498+
else if(src.id() == ID_get_may)
35003499
return convert_function(src, "__CPROVER_get_may", precedence=16);
35013500

35023501
else if(src.id()=="object_value")

‎src/goto-analyzer/taint_analysis.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ void taint_analysist::instrument(
159159
{
160160
case taint_parse_treet::rulet::SOURCE:
161161
{
162-
codet code_set_may("set_may");
162+
codet code_set_may(ID_set_may);
163163
code_set_may.operands().resize(2);
164164
code_set_may.op0()=where;
165165
code_set_may.op1()=
@@ -173,7 +173,7 @@ void taint_analysist::instrument(
173173
case taint_parse_treet::rulet::SINK:
174174
{
175175
goto_programt::targett t=insert_before.add_instruction();
176-
binary_predicate_exprt get_may("get_may");
176+
binary_predicate_exprt get_may(ID_get_may);
177177
get_may.op0()=where;
178178
get_may.op1()=address_of_exprt(string_constantt(rule.taint));
179179
t->make_assertion(not_exprt(get_may));
@@ -186,7 +186,7 @@ void taint_analysist::instrument(
186186

187187
case taint_parse_treet::rulet::SANITIZER:
188188
{
189-
codet code_clear_may("clear_may");
189+
codet code_clear_may(ID_clear_may);
190190
code_clear_may.operands().resize(2);
191191
code_clear_may.op0()=where;
192192
code_clear_may.op1()=

‎src/goto-instrument/thread_instrumentation.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ void thread_exit_instrumentation(goto_programt &goto_program)
4343
exprt mutex_locked_string=
4444
string_constantt("mutex-locked");
4545

46-
binary_exprt get_may("get_may");
46+
binary_exprt get_may(ID_get_may);
4747

4848
// NULL is any
4949
get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
@@ -89,8 +89,8 @@ void mutex_init_instrumentation(
8989
goto_programt &goto_program,
9090
typet lock_type)
9191
{
92-
symbol_tablet::symbolst::const_iterator f_it=
93-
symbol_table.symbols.find("__CPROVER_set_must");
92+
symbol_tablet::symbolst::const_iterator f_it =
93+
symbol_table.symbols.find(CPROVER_PREFIX "set_must");
9494

9595
if(f_it==symbol_table.symbols.end())
9696
return;

‎src/goto-programs/goto_inline_class.cpp

+6-6
Original file line numberDiff line numberDiff line change
@@ -720,12 +720,12 @@ const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive(
720720
bool goto_inlinet::is_ignored(const irep_idt id) const
721721
{
722722
return
723-
id=="__CPROVER_cleanup" ||
724-
id=="__CPROVER_set_must" ||
725-
id=="__CPROVER_set_may" ||
726-
id=="__CPROVER_clear_must" ||
727-
id=="__CPROVER_clear_may" ||
728-
id=="__CPROVER_cover";
723+
id == CPROVER_PREFIX "cleanup" ||
724+
id == CPROVER_PREFIX "set_must" ||
725+
id == CPROVER_PREFIX "set_may" ||
726+
id == CPROVER_PREFIX "clear_must" ||
727+
id == CPROVER_PREFIX "clear_may" ||
728+
id == CPROVER_PREFIX "cover";
729729
}
730730

731731
bool goto_inlinet::check_inline_map(

‎src/util/irep_ids.def

+6
Original file line numberDiff line numberDiff line change
@@ -849,6 +849,12 @@ IREP_ID_TWO(overflow_shl, overflow-shl)
849849
IREP_ID_ONE(lvsa_evs_type)
850850
IREP_ID_ONE(is_initializer)
851851
IREP_ID_TWO(C_is_taint_wrapper_type, #is_taint_wrapper_type)
852+
IREP_ID_ONE(get_may)
853+
IREP_ID_ONE(set_may)
854+
IREP_ID_ONE(clear_may)
855+
IREP_ID_ONE(get_must)
856+
IREP_ID_ONE(set_must)
857+
IREP_ID_ONE(clear_must)
852858

853859
#undef IREP_ID_ONE
854860
#undef IREP_ID_TWO

0 commit comments

Comments
 (0)