diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index ef97471298f..1deae4489b5 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -450,10 +450,9 @@ void custom_bitvector_domaint::transform( const auto &code = instruction.get_other(); const irep_idt &statement = code.get_statement(); - if(statement=="set_may" || - statement=="set_must" || - statement=="clear_may" || - statement=="clear_must") + if( + statement == ID_set_may || statement == ID_set_must || + statement == ID_clear_may || statement == ID_clear_must) { DATA_INVARIANT( code.operands().size() == 2, "set/clear_may/must has two operands"); @@ -463,13 +462,13 @@ void custom_bitvector_domaint::transform( // initialize to make Visual Studio happy modet mode = modet::SET_MUST; - if(statement=="set_must") + if(statement == ID_set_must) mode=modet::SET_MUST; - else if(statement=="clear_must") + else if(statement == ID_clear_must) mode=modet::CLEAR_MUST; - else if(statement=="set_may") + else if(statement == ID_set_may) mode=modet::SET_MAY; - else if(statement=="clear_may") + else if(statement == ID_clear_may) mode=modet::CLEAR_MAY; else UNREACHABLE; @@ -687,8 +686,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits) bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src) { - if(src.id()=="get_must" || - src.id()=="get_may") + if(src.id() == ID_get_must || src.id() == ID_get_may) return true; forall_operands(it, src) @@ -702,7 +700,7 @@ exprt custom_bitvector_domaint::eval( const exprt &src, custom_bitvector_analysist &custom_bitvector_analysis) const { - if(src.id()=="get_must" || src.id()=="get_may") + if(src.id() == ID_get_must || src.id() == ID_get_may) { if(src.operands().size()==2) { @@ -717,7 +715,7 @@ exprt custom_bitvector_domaint::eval( if(pointer.is_constant() && to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all { - if(src.id()=="get_may") + if(src.id() == ID_get_may) { for(const auto &bit : may_bits) if(get_bit(bit.second, bit_nr)) @@ -725,7 +723,7 @@ exprt custom_bitvector_domaint::eval( return false_exprt(); } - else if(src.id()=="get_must") + else if(src.id() == ID_get_must) { return false_exprt(); } @@ -739,9 +737,9 @@ exprt custom_bitvector_domaint::eval( bool value=false; - if(src.id()=="get_must") + if(src.id() == ID_get_must) value=get_bit(v.must_bits, bit_nr); - else if(src.id()=="get_may") + else if(src.id() == ID_get_may) value=get_bit(v.may_bits, bit_nr); if(value) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 7fb21e6ac62..87a7198933f 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2074,7 +2074,7 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); binary_predicate_exprt get_must_expr( - expr.arguments()[0], "get_must", expr.arguments()[1]); + expr.arguments()[0], ID_get_must, expr.arguments()[1]); get_must_expr.add_source_location()=source_location; return std::move(get_must_expr); @@ -2091,7 +2091,7 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); binary_predicate_exprt get_may_expr( - expr.arguments()[0], "get_may", expr.arguments()[1]); + expr.arguments()[0], ID_get_may, expr.arguments()[1]); get_may_expr.add_source_location()=source_location; return std::move(get_may_expr); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index b26ce493b11..87f015488e4 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2911,8 +2911,7 @@ std::string expr2ct::convert_code( if(statement==ID_array_replace) return convert_code_array_replace(src, indent); - if(statement=="set_may" || - statement=="set_must") + if(statement == ID_set_may || statement == ID_set_must) return indent_str(indent) + convert_function(src, id2string(statement)) + ";"; @@ -3451,10 +3450,10 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_pointer_object) return convert_function(src, "POINTER_OBJECT"); - else if(src.id()=="get_must") + else if(src.id() == ID_get_must) return convert_function(src, CPROVER_PREFIX "get_must"); - else if(src.id()=="get_may") + else if(src.id() == ID_get_may) return convert_function(src, CPROVER_PREFIX "get_may"); else if(src.id()=="object_value") diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 37999f064b8..57245c0cf5c 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -162,7 +162,7 @@ void taint_analysist::instrument( { case taint_parse_treet::rulet::SOURCE: { - codet code_set_may("set_may"); + codet code_set_may{ID_set_may}; code_set_may.operands().resize(2); code_set_may.op0() = where; code_set_may.op1() = @@ -174,10 +174,10 @@ void taint_analysist::instrument( case taint_parse_treet::rulet::SINK: { - binary_predicate_exprt get_may( + binary_predicate_exprt get_may{ where, - "get_may", - address_of_exprt(string_constantt(rule.taint))); + ID_get_may, + address_of_exprt(string_constantt(rule.taint))}; goto_programt::targett t = insert_before.add(goto_programt::make_assertion( not_exprt(get_may), instruction.source_location)); @@ -189,7 +189,7 @@ void taint_analysist::instrument( case taint_parse_treet::rulet::SANITIZER: { - codet code_clear_may("clear_may"); + codet code_clear_may{ID_clear_may}; code_clear_may.operands().resize(2); code_clear_may.op0() = where; code_clear_may.op1() = diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 06ee68d216c..5d49c71c72f 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -41,10 +41,10 @@ void thread_exit_instrumentation(goto_programt &goto_program) const string_constantt mutex_locked_string("mutex-locked"); // NULL is any - binary_predicate_exprt get_may( + binary_predicate_exprt get_may{ null_pointer_exprt(pointer_type(empty_typet())), - "get_may", - address_of_exprt(mutex_locked_string)); + ID_get_may, + address_of_exprt(mutex_locked_string)}; *end = goto_programt::make_assertion(not_exprt(get_may), source_location); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 18ffbd2ee2d..379becad8e2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -722,6 +722,12 @@ IREP_ID_ONE(to_member) IREP_ID_ONE(pointer_to_member) IREP_ID_ONE(tuple) IREP_ID_ONE(function_body) +IREP_ID_ONE(get_may) +IREP_ID_ONE(set_may) +IREP_ID_ONE(clear_may) +IREP_ID_ONE(get_must) +IREP_ID_ONE(set_must) +IREP_ID_ONE(clear_must) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree