diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp index 956840aa505..3fa48fda518 100644 --- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp +++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp @@ -1292,8 +1292,7 @@ codet character_refine_preprocesst::replace_character_call( { if(code.function().id()==ID_symbol) { - const irep_idt &function_id= - to_symbol_expr(code.function()).get_identifier(); + const irep_idt &function_id = to_symbol_expr(code.function()).identifier(); auto it=conversion_table.find(function_id); if(it!=conversion_table.end()) return (it->second)(code); diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index db24a2579c0..c565b16cda3 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -69,11 +69,10 @@ static bool references_class_model(const exprt &expr) for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it) { - if(can_cast_expr(*it) && - it->type() == class_type && - has_suffix( - id2string(to_symbol_expr(*it).get_identifier()), - JAVA_CLASS_MODEL_SUFFIX)) + if( + can_cast_expr(*it) && it->type() == class_type && + has_suffix( + id2string(to_symbol_expr(*it).identifier()), JAVA_CLASS_MODEL_SUFFIX)) { return true; } @@ -527,8 +526,8 @@ void ci_lazy_methodst::gather_needed_globals( // on an opaque type (i.e. we don't have the class definition at this point) // and will be created during the typecheck phase. // We don't mark it as 'needed' as it doesn't exist yet to keep. - const auto findit= - symbol_table.symbols.find(to_symbol_expr(e).get_identifier()); + const auto findit = + symbol_table.symbols.find(to_symbol_expr(e).identifier()); if(findit!=symbol_table.symbols.end() && findit->second.is_static_lifetime) { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 8d3c23d50f3..a6e650389dc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -206,7 +206,7 @@ exprt java_bytecode_convert_methodt::variable( const variablet &var= find_variable_for_slot(address, var_list); - if(!var.symbol_expr.get_identifier().empty()) + if(!var.symbol_expr.identifier().empty()) return var.symbol_expr; // an unnamed local variable @@ -952,7 +952,7 @@ static void gather_symbol_live_ranges( const auto &symexpr=to_symbol_expr(e); auto findit = result.emplace( std::piecewise_construct, - std::forward_as_tuple(symexpr.get_identifier()), + std::forward_as_tuple(symexpr.identifier()), std::forward_as_tuple(symexpr, pc, 1)); if(!findit.second) { @@ -1895,9 +1895,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) // Add anonymous locals to the symtab: for(const auto &var : used_local_names) { - symbolt new_symbol{var.get_identifier(), var.type(), ID_java}; + symbolt new_symbol{var.identifier(), var.type(), ID_java}; new_symbol.base_name=var.get(ID_C_base_name); - new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier()); + new_symbol.pretty_name = strip_java_namespace_prefix(var.identifier()); new_symbol.is_file_local=true; new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; @@ -1982,11 +1982,11 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) for(const auto &v : tmp_vars) vars_to_process.push_back( - &temporary_variable_live_ranges.at(v.get_identifier())); + &temporary_variable_live_ranges.at(v.identifier())); for(const auto &v : used_local_names) vars_to_process.push_back( - &temporary_variable_live_ranges.at(v.get_identifier())); + &temporary_variable_live_ranges.at(v.identifier())); for(const auto vp : vars_to_process) { @@ -2012,7 +2012,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) if(v.is_parameter) continue; // Skip anonymous variables: - if(v.symbol_expr.get_identifier().empty()) + if(v.symbol_expr.identifier().empty()) continue; auto &block = get_block_for_pcrange( root, @@ -2674,7 +2674,7 @@ code_blockt java_bytecode_convert_methodt::convert_putstatic( "stack_static_field", block, bytecode_write_typet::STATIC_FIELD, - symbol_expr.get_identifier()); + symbol_expr.identifier()); block.add(code_assignt(symbol_expr, op[0])); return block; } @@ -2834,7 +2834,7 @@ code_blockt java_bytecode_convert_methodt::convert_iinc( "stack_iinc", block, bytecode_write_typet::VARIABLE, - to_symbol_expr(locvar).get_identifier()); + to_symbol_expr(locvar).identifier()); const exprt arg1_int_type = typecast_exprt::conditional_cast(arg1, java_int_type()); @@ -3039,7 +3039,7 @@ code_blockt java_bytecode_convert_methodt::convert_store( const source_locationt &location) { const exprt var = variable(arg0, statement[0], address); - const irep_idt &var_name = to_symbol_expr(var).get_identifier(); + const irep_idt &var_name = to_symbol_expr(var).identifier(); code_blockt block; block.add_source_location() = location; @@ -3390,7 +3390,7 @@ void java_bytecode_convert_methodt::save_stack_entries( [&identifier](const exprt &expr) { const auto symbol_expr = expr_try_dynamic_cast(expr); return !symbol_expr ? tvt::unknown() - : tvt(symbol_expr->get_identifier() == identifier); + : tvt(symbol_expr->identifier() == identifier); }; // Function that checks whether the expression is a dereference diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 9f3497313f5..b982ff625b0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -518,10 +518,10 @@ static symbol_exprt get_or_create_class_literal_symbol( symbol_exprt symbol_expr( id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX, java_lang_Class); - if(!symbol_table.has_symbol(symbol_expr.get_identifier())) + if(!symbol_table.has_symbol(symbol_expr.identifier())) { symbolt new_class_symbol{ - symbol_expr.get_identifier(), symbol_expr.type(), ID_java}; + symbol_expr.identifier(), symbol_expr.type(), ID_java}; INVARIANT( new_class_symbol.name.starts_with("java::"), "class identifier should have 'java::' prefix"); @@ -1241,7 +1241,7 @@ static void notify_static_method_calls( const symbol_exprt *fn_sym = expr_try_dynamic_cast(fn_call->function()); if(fn_sym) - needed_lazy_methods->add_needed_method(fn_sym->get_identifier()); + needed_lazy_methods->add_needed_method(fn_sym->identifier()); } else if( it->id() == ID_side_effect && diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 2fe7ccafbf7..28f8439c48f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -636,7 +636,7 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value) { if(const auto &symbol_expr = expr_try_dynamic_cast(value)) { - const irep_idt &value_id = symbol_expr->get_identifier(); + const irep_idt &value_id = symbol_expr->identifier(); get_class_refs_rec(*java_type_from_string(id2string(value_id))); } else if(const auto &array_expr = expr_try_dynamic_cast(value)) diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 682ec957091..254aed3c79b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -67,7 +67,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array( void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr) { - const irep_idt &identifier = expr.get_identifier(); + const irep_idt &identifier = expr.identifier(); // the java_bytecode_convert_class and java_bytecode_convert_method made sure // "identifier" exists in the symbol table diff --git a/jbmc/src/java_bytecode/java_trace_validation.cpp b/jbmc/src/java_bytecode/java_trace_validation.cpp index 2680c4c1276..1c8f3526b0a 100644 --- a/jbmc/src/java_bytecode/java_trace_validation.cpp +++ b/jbmc/src/java_bytecode/java_trace_validation.cpp @@ -21,7 +21,7 @@ Author: Jeannie Moulton bool check_symbol_structure(const exprt &expr) { const auto symbol = expr_try_dynamic_cast(expr); - return symbol && !symbol->get_identifier().empty(); + return symbol && !symbol->identifier().empty(); } /// \return true iff the expression is a symbol or is an expression whose first diff --git a/jbmc/src/java_bytecode/lift_clinit_calls.cpp b/jbmc/src/java_bytecode/lift_clinit_calls.cpp index 8fe098d5130..d3e9db84ed1 100644 --- a/jbmc/src/java_bytecode/lift_clinit_calls.cpp +++ b/jbmc/src/java_bytecode/lift_clinit_calls.cpp @@ -34,7 +34,7 @@ codet lift_clinit_calls(codet input) const auto callee = expr_try_dynamic_cast( to_code_function_call(*code).function())) { - if(is_clinit_wrapper_function(callee->get_identifier())) + if(is_clinit_wrapper_function(callee->identifier())) { clinit_wrappers_called.push_back(*callee); // Replace call with skip: diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index e745d0beaf8..0153aeb0d00 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -200,8 +200,8 @@ bool remove_exceptionst::function_or_callees_may_throw( DATA_INVARIANT( function_expr.id()==ID_symbol, "identifier expected to be a symbol"); - const irep_idt &function_name= - to_symbol_expr(function_expr).get_identifier(); + const irep_idt &function_name = + to_symbol_expr(function_expr).identifier(); if(function_may_throw(function_name)) return true; } @@ -441,7 +441,7 @@ remove_exceptionst::instrument_function_call( DATA_INVARIANT( function.id() == ID_symbol, "function call expected to be a symbol"); - const irep_idt &callee_id = to_symbol_expr(function).get_identifier(); + const irep_idt &callee_id = to_symbol_expr(function).identifier(); if(function_may_throw(callee_id)) { diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index 05377e0c167..5615983aa24 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -68,7 +68,7 @@ static nondet_instruction_infot is_nondet_returning_object(const code_function_callt &function_call) { const auto &function_symbol = to_symbol_expr(function_call.function()); - const auto function_name = id2string(function_symbol.get_identifier()); + const auto function_name = id2string(function_symbol.identifier()); const std::regex reg( R"(.*org\.cprover\.CProver\.nondet)" R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))"); @@ -108,7 +108,7 @@ get_nondet_instruction_info(const goto_programt::const_targett &instr) static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier) { return expr.id() == ID_symbol && - to_symbol_expr(expr).get_identifier() == identifier; + to_symbol_expr(expr).identifier() == identifier; } /// Return whether the expression is a typecast with the specified identifier. @@ -129,7 +129,7 @@ static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier) } const auto &op_symbol = to_symbol_expr(typecast.op()); // Return whether the typecast has the expected operand - return op_symbol.get_identifier() == identifier; + return op_symbol.identifier() == identifier; } /// Return whether the instruction is an assignment, and the rhs is a symbol or @@ -214,7 +214,7 @@ static goto_programt::targett check_and_replace_target( irep_idt return_identifier; if(remove_returns_not_run) { - return_identifier = to_symbol_expr(target->call_lhs()).get_identifier(); + return_identifier = to_symbol_expr(target->call_lhs()).identifier(); } else { @@ -236,8 +236,7 @@ static goto_programt::targett check_and_replace_target( } // Otherwise it's the temporary variable. - return_identifier = - to_symbol_expr(return_value_assignment).get_identifier(); + return_identifier = to_symbol_expr(return_value_assignment).identifier(); } // Look for the assignment of the temporary return variable into our target diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index af01baa8159..82721843801 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -64,7 +64,7 @@ static bool is_call_to( const exprt &callee_expr = inst->call_function(); if(callee_expr.id() != ID_symbol) return false; - return to_symbol_expr(callee_expr).get_identifier() == callee; + return to_symbol_expr(callee_expr).identifier() == callee; } static bool is_assume_false(goto_programt::const_targett inst) diff --git a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp index a505fed318e..30f57f2b615 100644 --- a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp +++ b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp @@ -22,9 +22,10 @@ Author: Diffblue Ltd. static bool contains_symbol_reference(const exprt &expr, const irep_idt &id) { return std::any_of( - expr.depth_begin(), expr.depth_end(), [id](const exprt &e) { - return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == id; - }); + expr.depth_begin(), + expr.depth_end(), + [id](const exprt &e) + { return e.id() == ID_symbol && to_symbol_expr(e).identifier() == id; }); } SCENARIO( diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp index 49cd0a3ba9b..af47847e992 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp @@ -55,7 +55,7 @@ void validate_lambda_assignment( const symbol_exprt &rhs_symbol = require_expr::require_symbol(rhs_value.op()); - const irep_idt &tmp_object_symbol = rhs_symbol.get_identifier(); + const irep_idt &tmp_object_symbol = rhs_symbol.identifier(); const auto tmp_object_assignments = require_goto_statements::find_pointer_assignments( @@ -135,8 +135,8 @@ void validate_lambda_assignment( if(it->id() == ID_symbol) { symbol_exprt &symbol_expr = to_symbol_expr(it.mutate()); - const irep_idt simple_id = symbol_expr.get_identifier(); - symbol_expr.set_identifier(variable_prefix + id2string(simple_id)); + const irep_idt simple_id = symbol_expr.identifier(); + symbol_expr.identifier(variable_prefix + id2string(simple_id)); } } } diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index cd97726bb07..7509b736f2a 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -320,8 +320,7 @@ SCENARIO( { if( symbol_expr->source_location().get_java_bytecode_index() == "0" && - symbol_expr->get_identifier() == - "java::ClassReadingStaticField.x") + symbol_expr->identifier() == "java::ClassReadingStaticField.x") found = true; } }); @@ -1029,12 +1028,12 @@ TEST_CASE( // Assert side effects on variables REQUIRE(variables.size() == 3); REQUIRE( - variables[0][0].symbol_expr.get_identifier() == + variables[0][0].symbol_expr.identifier() == id2string(method_id) + "::this"); REQUIRE( - variables[1][0].symbol_expr.get_identifier() == + variables[1][0].symbol_expr.identifier() == id2string(method_id) + "::this$0"); REQUIRE( - variables[2][0].symbol_expr.get_identifier() == + variables[2][0].symbol_expr.identifier() == id2string(method_id) + "::other"); } diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp index 7b7d6b3a098..6ea155a486d 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp @@ -90,8 +90,7 @@ SCENARIO( REQUIRE(annotations.size() == 1); const auto &annotation = annotations.front(); const auto &element_value_pair = annotation.element_value_pairs.front(); - const auto &id = - to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &id = to_symbol_expr(element_value_pair.value).identifier(); const auto &java_type = java_type_from_string(id2string(id)); const std::string &class_name = id2string( to_struct_tag_type(to_reference_type(*java_type).base_type()) @@ -116,8 +115,7 @@ SCENARIO( REQUIRE(annotations.size() == 1); const auto &annotation = annotations.front(); const auto &element_value_pair = annotation.element_value_pairs.front(); - const auto &id = - to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &id = to_symbol_expr(element_value_pair.value).identifier(); const auto &java_type = java_type_from_string(id2string(id)); REQUIRE(*java_type == java_byte_type()); } @@ -138,8 +136,7 @@ SCENARIO( REQUIRE(annotations.size() == 1); const auto &annotation = annotations.front(); const auto &element_value_pair = annotation.element_value_pairs.front(); - const auto &id = - to_symbol_expr(element_value_pair.value).get_identifier(); + const auto &id = to_symbol_expr(element_value_pair.value).identifier(); const auto &java_type = java_type_from_string(id2string(id)); REQUIRE(*java_type == java_void_type()); } diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index f6ec3b17f85..2ad12a18031 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -67,7 +67,7 @@ void validate_nondet_method_removed( if(function.id() != ID_symbol) continue; - const irep_idt function_id = to_symbol_expr(function).get_identifier(); + const irep_idt function_id = to_symbol_expr(function).identifier(); if( function_id == "java::org.cprover.CProver.nondetWithoutNull:()" diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp index 15598ef8e7b..3365faee7a6 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp @@ -126,7 +126,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == "symbol_to_assign"); + .identifier() == "symbol_to_assign"); } THEN("The instruction zero-initializes the struct") { @@ -226,7 +226,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == "symbol_to_assign"); + .identifier() == "symbol_to_assign"); } THEN("The instruction zero-initializes the struct") @@ -259,7 +259,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == + .identifier() == "java::TestClass.:()V::user_specified_array_data_init"); } THEN("The instruction assigns the array cell to 42") @@ -358,7 +358,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == "symbol_to_assign"); + .identifier() == "symbol_to_assign"); } THEN("The instruction zero-initializes the struct") @@ -412,7 +412,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == + .identifier() == "java::TestClass.:()V::user_specified_array_data_init"); } THEN("The instruction assigns the array cell to 42") @@ -556,7 +556,7 @@ SCENARIO( .as()[0] .as() .get() - .get_identifier() == "symbol_to_assign"); + .identifier() == "symbol_to_assign"); } THEN( "zero-initialize the object:" diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp index 70849a02558..9efae038481 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp @@ -93,7 +93,7 @@ SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]") const exprt function_called = make_query(clinit_body)[0].as().get().function(); REQUIRE( - make_query(function_called).as().get().get_identifier() == + make_query(function_called).as().get().identifier() == clinit_symbol.name); } } @@ -175,10 +175,8 @@ SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]") { auto assignment = make_query(clinit_body)[0].as().get(); REQUIRE( - make_query(assignment.lhs()) - .as() - .get() - .get_identifier() == "field_name_for_codet"); + make_query(assignment.lhs()).as().get().identifier() == + "field_name_for_codet"); REQUIRE(assignment.rhs() == from_integer(42, java_int_type())); } } diff --git a/jbmc/unit/java_bytecode/java_string_literals.cpp b/jbmc/unit/java_bytecode/java_string_literals.cpp index 009f911ea27..0eb6a9a8691 100644 --- a/jbmc/unit/java_bytecode/java_string_literals.cpp +++ b/jbmc/unit/java_bytecode/java_string_literals.cpp @@ -28,7 +28,7 @@ TEST_CASE( generate_class_stub("java.lang.String", symbol_table, message_handler, {}); REQUIRE(symbol_table.lookup( get_or_create_string_literal_symbol("foo", symbol_table, false) - .get_identifier())); + .identifier())); create_java_initialize(symbol_table); symbol_table.get_writeable_ref(INITIALIZE_FUNCTION).value = code_blockt{}; diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp index 032e258d1a0..019b9a34509 100644 --- a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp +++ b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp @@ -35,8 +35,7 @@ void check_function_call( REQUIRE(target->type() == goto_program_instruction_typet::FUNCTION_CALL); REQUIRE(target->call_function().id() == ID_symbol); REQUIRE( - to_symbol_expr(target->call_function()).get_identifier() == - function_name); + to_symbol_expr(target->call_function()).identifier() == function_name); } } diff --git a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 85d255eb5a8..92cca9f876c 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp @@ -39,7 +39,7 @@ class test_value_sett:public value_sett { if(assign.lhs().id()!=ID_symbol) return false; - const irep_idt &id=to_symbol_expr(assign.lhs()).get_identifier(); + const irep_idt &id = to_symbol_expr(assign.lhs()).identifier(); return id2string(id).find("ignored")!=std::string::npos; } @@ -67,7 +67,7 @@ class test_value_sett:public value_sett // Disregard writes against variables containing 'no_write': if(lhs.id()==ID_symbol) { - const irep_idt &id=to_symbol_expr(lhs).get_identifier(); + const irep_idt &id = to_symbol_expr(lhs).identifier(); if(id2string(id).find("no_write")!=std::string::npos) return; } @@ -106,7 +106,7 @@ class test_value_sett:public value_sett exprt read_sym = skip_typecast(expr); if(read_sym.id()==ID_symbol) { - const irep_idt &id=to_symbol_expr(read_sym).get_identifier(); + const irep_idt &id = to_symbol_expr(read_sym).identifier(); if(id2string(id).find("maybe_unknown")!=std::string::npos) insert(dest, exprt(ID_unknown, read_sym.type())); } @@ -121,7 +121,7 @@ class test_value_sett:public value_sett // variable "effect": if(lhs.id()==ID_symbol) { - const irep_idt &id=to_symbol_expr(lhs).get_identifier(); + const irep_idt &id = to_symbol_expr(lhs).identifier(); const auto &id_str=id2string(id); auto find_idx=id_str.find("cause"); if(find_idx!=std::string::npos) diff --git a/jbmc/unit/util/simplify_expr.cpp b/jbmc/unit/util/simplify_expr.cpp index 5e1ec18b059..05cea1d77a7 100644 --- a/jbmc/unit/util/simplify_expr.cpp +++ b/jbmc/unit/util/simplify_expr.cpp @@ -33,7 +33,7 @@ void test_unnecessary_cast(const typet &type) REQUIRE(simplified.id()==ID_symbol); REQUIRE(simplified.type()==type); const auto &symbol=to_symbol_expr(simplified); - REQUIRE(symbol.get_identifier()=="foo"); + REQUIRE(symbol.identifier() == "foo"); } WHEN("Casts should remain, they are left untouched") diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 3fd897c0d14..13330dfbd87 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -465,7 +465,7 @@ bool ai_baset::visit_function_call( if(callee_expression.id() == ID_symbol) { const irep_idt &callee_function_id = - to_symbol_expr(callee_expression).get_identifier(); + to_symbol_expr(callee_expression).identifier(); log.progress() << "Calling " << callee_function_id << messaget::eom; diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 543e68302a4..27c13458271 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -61,7 +61,7 @@ static void forall_callsites( PRECONDITION_WITH_DIAGNOSTICS( function_expr.id() == ID_symbol, "call graph computation requires function pointer removal"); - const irep_idt &callee = to_symbol_expr(function_expr).get_identifier(); + const irep_idt &callee = to_symbol_expr(function_expr).identifier(); call_task(i_it, callee); } } diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index c57466bea2c..d0fb72f8f0e 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -200,7 +200,7 @@ void constant_propagator_domaint::transform( { // called function identifier const symbol_exprt &symbol_expr=to_symbol_expr(function); - const irep_idt id=symbol_expr.get_identifier(); + const irep_idt id = symbol_expr.identifier(); // Functions with no body if(function_from == function_to) @@ -435,7 +435,7 @@ class constant_propagator_can_forward_propagatet : public can_forward_propagatet bool is_constant(const exprt &expr) const override { if(expr.id() == ID_symbol) - return is_constant(to_symbol_expr(expr).get_identifier()); + return is_constant(to_symbol_expr(expr).identifier()); return can_forward_propagatet::is_constant(expr); } @@ -462,7 +462,7 @@ bool constant_propagator_domaint::valuest::is_constant( bool constant_propagator_domaint::valuest::set_to_top( const symbol_exprt &symbol_expr) { - const auto n_erased = replace_const.erase(symbol_expr.get_identifier()); + const auto n_erased = replace_const.erase(symbol_expr.identifier()); INVARIANT(n_erased==0 || !is_bottom, "bottom should have no elements at all"); diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index c56d92f431f..6e3a56a16e7 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -60,7 +60,7 @@ irep_idt custom_bitvector_domaint::object2id(const exprt &src) { if(src.id()==ID_symbol) { - return to_symbol_expr(src).get_identifier(); + return to_symbol_expr(src).identifier(); } else if(src.id()==ID_dereference) { @@ -317,72 +317,72 @@ void custom_bitvector_domaint::transform( if(function.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); - if( - identifier == CPROVER_PREFIX "set_must" || - identifier == CPROVER_PREFIX "clear_must" || - identifier == CPROVER_PREFIX "set_may" || - identifier == CPROVER_PREFIX "clear_may") + if( + identifier == CPROVER_PREFIX "set_must" || + identifier == CPROVER_PREFIX "clear_must" || + identifier == CPROVER_PREFIX "set_may" || + identifier == CPROVER_PREFIX "clear_may") + { + if(instruction.call_arguments().size() == 2) { - if(instruction.call_arguments().size() == 2) - { - unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]); - - // initialize to make Visual Studio happy - modet mode = modet::SET_MUST; - - if(identifier == CPROVER_PREFIX "set_must") - mode=modet::SET_MUST; - else if(identifier == CPROVER_PREFIX "clear_must") - mode=modet::CLEAR_MUST; - else if(identifier == CPROVER_PREFIX "set_may") - mode=modet::SET_MAY; - else if(identifier == CPROVER_PREFIX "clear_may") - mode=modet::CLEAR_MAY; - else - UNREACHABLE; + unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]); + + // initialize to make Visual Studio happy + modet mode = modet::SET_MUST; + + if(identifier == CPROVER_PREFIX "set_must") + mode = modet::SET_MUST; + else if(identifier == CPROVER_PREFIX "clear_must") + mode = modet::CLEAR_MUST; + else if(identifier == CPROVER_PREFIX "set_may") + mode = modet::SET_MAY; + else if(identifier == CPROVER_PREFIX "clear_may") + mode = modet::CLEAR_MAY; + else + UNREACHABLE; - exprt lhs = instruction.call_arguments()[0]; + exprt lhs = instruction.call_arguments()[0]; - if(lhs.type().id()==ID_pointer) + if(lhs.type().id() == ID_pointer) + { + if( + lhs.is_constant() && + to_constant_expr(lhs).is_null_pointer()) // NULL means all { - if( - lhs.is_constant() && - to_constant_expr(lhs).is_null_pointer()) // NULL means all + if(mode == modet::CLEAR_MAY) { - if(mode==modet::CLEAR_MAY) - { - for(auto &bit : may_bits) - clear_bit(bit.second, bit_nr); - - // erase blank ones - erase_blank_vectors(may_bits); - } - else if(mode==modet::CLEAR_MUST) - { - for(auto &bit : must_bits) - clear_bit(bit.second, bit_nr); - - // erase blank ones - erase_blank_vectors(must_bits); - } + for(auto &bit : may_bits) + clear_bit(bit.second, bit_nr); + + // erase blank ones + erase_blank_vectors(may_bits); } - else + else if(mode == modet::CLEAR_MUST) { - dereference_exprt deref(lhs); + for(auto &bit : must_bits) + clear_bit(bit.second, bit_nr); - // may alias other stuff - std::set lhs_set=cba.aliases(deref, from); + // erase blank ones + erase_blank_vectors(must_bits); + } + } + else + { + dereference_exprt deref(lhs); - for(const auto &l : lhs_set) - { - set_bit(l, bit_nr, mode); - } + // may alias other stuff + std::set lhs_set = cba.aliases(deref, from); + + for(const auto &l : lhs_set) + { + set_bit(l, bit_nr, mode); } } } } + } else if(identifier=="memcpy" || identifier=="memmove") { diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp index d9f849b7e9f..941d6b79622 100644 --- a/src/analyses/dirty.cpp +++ b/src/analyses/dirty.cpp @@ -74,7 +74,7 @@ void dirtyt::find_dirty_address_of(const exprt &expr) { if(expr.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(expr).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr).identifier(); dirty.insert(identifier); } diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index 47a67511c2f..0f91890e333 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -72,7 +72,7 @@ class dirtyt bool operator()(const symbol_exprt &expr) const { die_if_uninitialized(); - return operator()(expr.get_identifier()); + return operator()(expr.identifier()); } const std::unordered_set &get_dirty_ids() const diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 94ae7556d24..5e85c86248c 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com bool escape_domaint::is_tracked(const symbol_exprt &symbol) { - const irep_idt &identifier=symbol.get_identifier(); + const irep_idt &identifier = symbol.identifier(); if( identifier == CPROVER_PREFIX "memory_leak" || identifier == CPROVER_PREFIX "dead_object" || @@ -36,7 +36,7 @@ irep_idt escape_domaint::get_function(const exprt &lhs) return get_function(to_typecast_expr(lhs).op()); else if(lhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(lhs).get_identifier(); + irep_idt identifier = to_symbol_expr(lhs).identifier(); return identifier; } @@ -52,7 +52,7 @@ void escape_domaint::assign_lhs_cleanup( const symbol_exprt &symbol_expr=to_symbol_expr(lhs); if(is_tracked(symbol_expr)) { - irep_idt identifier=symbol_expr.get_identifier(); + irep_idt identifier = symbol_expr.identifier(); if(cleanup_functions.empty()) cleanup_map.erase(identifier); @@ -71,7 +71,7 @@ void escape_domaint::assign_lhs_aliases( const symbol_exprt &symbol_expr=to_symbol_expr(lhs); if(is_tracked(symbol_expr)) { - irep_idt identifier=symbol_expr.get_identifier(); + irep_idt identifier = symbol_expr.identifier(); aliases.isolate(identifier); @@ -92,7 +92,7 @@ void escape_domaint::get_rhs_cleanup( const symbol_exprt &symbol_expr=to_symbol_expr(rhs); if(is_tracked(symbol_expr)) { - irep_idt identifier=symbol_expr.get_identifier(); + irep_idt identifier = symbol_expr.identifier(); const escape_domaint::cleanup_mapt::const_iterator m_it= cleanup_map.find(identifier); @@ -122,7 +122,7 @@ void escape_domaint::get_rhs_aliases( const symbol_exprt &symbol_expr=to_symbol_expr(rhs); if(is_tracked(symbol_expr)) { - irep_idt identifier=symbol_expr.get_identifier(); + irep_idt identifier = symbol_expr.identifier(); alias_set.insert(identifier); for(const auto &alias : aliases) @@ -151,7 +151,7 @@ void escape_domaint::get_rhs_aliases_address_of( { if(rhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(rhs).get_identifier(); + irep_idt identifier = to_symbol_expr(rhs).identifier(); alias_set.insert("&"+id2string(identifier)); } else if(rhs.id()==ID_if) @@ -201,14 +201,14 @@ void escape_domaint::transform( break; case DECL: - aliases.isolate(instruction.decl_symbol().get_identifier()); - assign_lhs_cleanup(instruction.decl_symbol(), std::set()); - break; + aliases.isolate(instruction.decl_symbol().identifier()); + assign_lhs_cleanup(instruction.decl_symbol(), std::set()); + break; case DEAD: - aliases.isolate(instruction.dead_symbol().get_identifier()); - assign_lhs_cleanup(instruction.dead_symbol(), std::set()); - break; + aliases.isolate(instruction.dead_symbol().identifier()); + assign_lhs_cleanup(instruction.dead_symbol(), std::set()); + break; case FUNCTION_CALL: { @@ -216,30 +216,30 @@ void escape_domaint::transform( if(function.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - if(identifier == CPROVER_PREFIX "cleanup") + const irep_idt &identifier = to_symbol_expr(function).identifier(); + if(identifier == CPROVER_PREFIX "cleanup") + { + if(instruction.call_arguments().size() == 2) { - if(instruction.call_arguments().size() == 2) - { - exprt lhs = instruction.call_arguments()[0]; + exprt lhs = instruction.call_arguments()[0]; - irep_idt cleanup_function = - get_function(instruction.call_arguments()[1]); + irep_idt cleanup_function = + get_function(instruction.call_arguments()[1]); - if(!cleanup_function.empty()) + if(!cleanup_function.empty()) + { + // may alias other stuff + std::set lhs_set; + get_rhs_aliases(lhs, lhs_set); + + for(const auto &l : lhs_set) { - // may alias other stuff - std::set lhs_set; - get_rhs_aliases(lhs, lhs_set); - - for(const auto &l : lhs_set) - { - cleanup_map[l].cleanup_functions.insert(cleanup_function); - } + cleanup_map[l].cleanup_functions.insert(cleanup_function); } } } } + } } break; @@ -382,7 +382,7 @@ void escape_domaint::check_lhs( { if(lhs.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(lhs).get_identifier(); + const irep_idt &identifier = to_symbol_expr(lhs).identifier(); // pointer with cleanup function? const escape_domaint::cleanup_mapt::const_iterator m_it= @@ -477,7 +477,7 @@ void escape_analysist::instrument( const escape_domaint &d = operator[](i_it); const escape_domaint::cleanup_mapt::const_iterator m_it = - d.cleanup_map.find("&" + id2string(dead_symbol.get_identifier())); + d.cleanup_map.find("&" + id2string(dead_symbol.identifier())); // does it have a cleanup function for the object? if(m_it != d.cleanup_map.end()) diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index 2aa7f41bb88..23baf81a93f 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -282,7 +282,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec( if(function.id()==ID_symbol) { - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); if(recursion_set.find(identifier)!=recursion_set.end()) { diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 47b1dcb40b9..812737517ec 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -24,7 +24,7 @@ void global_may_alias_domaint::assign_lhs_aliases( { if(lhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(lhs).get_identifier(); + irep_idt identifier = to_symbol_expr(lhs).identifier(); aliases.isolate(identifier); @@ -46,7 +46,7 @@ void global_may_alias_domaint::get_rhs_aliases( { if(rhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(rhs).get_identifier(); + irep_idt identifier = to_symbol_expr(rhs).identifier(); alias_set.insert(identifier); for(const auto &alias : alias_set) @@ -79,7 +79,7 @@ void global_may_alias_domaint::get_rhs_aliases_address_of( { if(rhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(rhs).get_identifier(); + irep_idt identifier = to_symbol_expr(rhs).identifier(); alias_set.insert("&"+id2string(identifier)); } else if(rhs.id()==ID_if) @@ -118,11 +118,11 @@ void global_may_alias_domaint::transform( } case DECL: - aliases.isolate(instruction.decl_symbol().get_identifier()); + aliases.isolate(instruction.decl_symbol().identifier()); break; case DEAD: - aliases.isolate(instruction.dead_symbol().get_identifier()); + aliases.isolate(instruction.dead_symbol().identifier()); break; case FUNCTION_CALL: // Probably safe diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 9dc4f2eae42..312540e22e7 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -585,7 +585,7 @@ void rw_range_sett::get_objects_rec( else if(expr.id()==ID_symbol) { const symbol_exprt &symbol=to_symbol_expr(expr); - const irep_idt identifier=symbol.get_identifier(); + const irep_idt identifier = symbol.identifier(); auto symbol_bits = pointer_offset_bits(symbol.type(), ns); diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index d6bd97d28ba..dcc22a1ac34 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -223,7 +223,7 @@ void interval_domaint::havoc_rec(const exprt &lhs) } else if(lhs.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(lhs).get_identifier(); + irep_idt identifier = to_symbol_expr(lhs).identifier(); if(is_int(lhs.type())) int_map.erase(identifier); @@ -274,7 +274,7 @@ void interval_domaint::assume_rec( if(lhs.id() == ID_symbol && rhs.is_constant()) { - irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier(); + irep_idt lhs_identifier = to_symbol_expr(lhs).identifier(); if(is_int(lhs.type()) && is_int(rhs.type())) { @@ -299,7 +299,7 @@ void interval_domaint::assume_rec( } else if(lhs.is_constant() && rhs.id() == ID_symbol) { - irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier(); + irep_idt rhs_identifier = to_symbol_expr(rhs).identifier(); if(is_int(lhs.type()) && is_int(rhs.type())) { @@ -324,8 +324,8 @@ void interval_domaint::assume_rec( } else if(lhs.id()==ID_symbol && rhs.id()==ID_symbol) { - irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier(); - irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier(); + irep_idt lhs_identifier = to_symbol_expr(lhs).identifier(); + irep_idt rhs_identifier = to_symbol_expr(rhs).identifier(); if(is_int(lhs.type()) && is_int(rhs.type())) { @@ -409,7 +409,7 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const { if(is_int(src.type())) { - int_mapt::const_iterator i_it=int_map.find(src.get_identifier()); + int_mapt::const_iterator i_it = int_map.find(src.identifier()); if(i_it==int_map.end()) return true_exprt(); @@ -437,7 +437,7 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const } else if(is_float(src.type())) { - float_mapt::const_iterator i_it=float_map.find(src.get_identifier()); + float_mapt::const_iterator i_it = float_map.find(src.identifier()); if(i_it==float_map.end()) return true_exprt(); diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index f369177b886..26eca1aef50 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -142,7 +142,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const } if(expr.id()==ID_symbol) - return id2string(to_symbol_expr(expr).get_identifier()); + return id2string(to_symbol_expr(expr).identifier()); return ""; } diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 74f4137cbf0..20907f36f5f 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -67,7 +67,7 @@ void local_bitvector_analysist::assign_lhs( { if(lhs.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(lhs).get_identifier(); + const irep_idt &identifier = to_symbol_expr(lhs).identifier(); if(is_tracked(identifier)) { @@ -122,7 +122,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec( } else if(rhs.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(rhs).get_identifier(); + const irep_idt &identifier = to_symbol_expr(rhs).identifier(); if(is_tracked(identifier)) { const auto src_pointer = pointers.number(identifier); @@ -137,7 +137,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec( if(object.id()==ID_symbol) { - if(locals.is_local(to_symbol_expr(object).get_identifier())) + if(locals.is_local(to_symbol_expr(object).identifier())) return flagst::mk_dynamic_local(); else return flagst::mk_static_lifetime(); @@ -147,8 +147,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec( const index_exprt &index_expr=to_index_expr(object); if(index_expr.array().id()==ID_symbol) { - if(locals.is_local( - to_symbol_expr(index_expr.array()).get_identifier())) + if(locals.is_local(to_symbol_expr(index_expr.array()).identifier())) return flagst::mk_dynamic_local() | flagst::mk_uses_offset(); else return flagst::mk_static_lifetime() | flagst::mk_uses_offset(); diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index fe45d512c0c..967ea924d2a 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -80,8 +80,7 @@ void local_may_aliast::assign_lhs( { if(objects[i].id()==ID_symbol) { - const irep_idt &identifier= - to_symbol_expr(objects[i]).get_identifier(); + const irep_idt &identifier = to_symbol_expr(objects[i]).identifier(); if(dirty(identifier) || !locals.is_local(identifier)) { @@ -404,8 +403,7 @@ void local_may_aliast::build(const goto_functiont &goto_function) { if(objects[i].id() == ID_symbol) { - const irep_idt &identifier = - to_symbol_expr(objects[i]).get_identifier(); + const irep_idt &identifier = to_symbol_expr(objects[i]).identifier(); if(dirty(identifier) || !locals.is_local(identifier)) { @@ -485,7 +483,7 @@ void local_may_aliast::output( INVARIANT(j < objects.size(), "invalid object index"); irep_idt identifier; if(objects[j].id() == ID_symbol) - identifier = to_symbol_expr(objects[j]).get_identifier(); + identifier = to_symbol_expr(objects[j]).identifier(); out << ' ' << from_expr(ns, identifier, objects[j]); } diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index a20739c4c8a..c0b10ed3893 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -20,7 +20,7 @@ void localst::build(const goto_functiont &goto_function) for(const auto &instruction : goto_function.body.instructions) { if(instruction.is_decl()) - locals.insert(instruction.decl_symbol().get_identifier()); + locals.insert(instruction.decl_symbol().identifier()); } locals.insert( diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index f44562ed90f..c5d4adeb209 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -139,7 +139,7 @@ void rd_range_domaint::transform_dead( const namespacet &, locationt from) { - const irep_idt &identifier = from->dead_symbol().get_identifier(); + const irep_idt &identifier = from->dead_symbol().identifier(); valuest::iterator entry=values.find(identifier); @@ -184,7 +184,7 @@ void rd_range_domaint::transform_function_call( { // only if there is an actual call, i.e., we have a body const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function()); - if(function_to == fn_symbol_expr.get_identifier()) + if(function_to == fn_symbol_expr.identifier()) { for(valuest::iterator it=values.begin(); it!=values.end(); @@ -209,8 +209,8 @@ void rd_range_domaint::transform_function_call( ++it; } - const code_typet &code_type= - to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type); + const code_typet &code_type = + to_code_type(ns.lookup(fn_symbol_expr.identifier()).type); for(const auto ¶m : code_type.parameters()) { diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index f328438a03b..aa6b3c0e6e4 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -123,8 +123,7 @@ void uncaught_exceptions_domaint::transform( DATA_INVARIANT( function_expr.id()==ID_symbol, "identifier expected to be a symbol"); - const irep_idt &function_name= - to_symbol_expr(function_expr).get_identifier(); + const irep_idt &function_name = to_symbol_expr(function_expr).identifier(); // use the current information about the callee join(uea.exceptions_map[function_name]); break; diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 3513c3af66e..fef7b2a8708 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -32,7 +32,7 @@ void uninitialized_domaint::transform( if(from->is_decl()) { - const irep_idt &identifier = from->decl_symbol().get_identifier(); + const irep_idt &identifier = from->decl_symbol().identifier(); const symbolt &symbol = ns.lookup(identifier); if(!symbol.is_static_lifetime) @@ -59,7 +59,7 @@ void uninitialized_domaint::assign(const exprt &lhs) else if(lhs.id()==ID_member) assign(to_member_expr(lhs).struct_op()); else if(lhs.id()==ID_symbol) - uninitialized.erase(to_symbol_expr(lhs).get_identifier()); + uninitialized.erase(to_symbol_expr(lhs).identifier()); } void uninitialized_domaint::output( diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index ab06589e902..c5fa3a3f6fd 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -144,7 +144,7 @@ abstract_object_pointert abstract_environmentt::resolve_symbol( const namespacet &ns) const { const symbol_exprt &symbol(to_symbol_expr(expr)); - const auto symbol_entry = map.find(symbol.get_identifier()); + const auto symbol_entry = map.find(symbol.identifier()); if(symbol_entry.has_value()) return symbol_entry.value(); @@ -233,8 +233,8 @@ bool abstract_environmentt::assign( if(final_value != lhs_value) { - CHECK_RETURN(!symbol_expr.get_identifier().empty()); - map.insert_or_replace(symbol_expr.get_identifier(), final_value); + CHECK_RETURN(!symbol_expr.identifier().empty()); + map.insert_or_replace(symbol_expr.identifier(), final_value); } } return true; @@ -480,7 +480,7 @@ abstract_object_pointert abstract_environmentt::eval_expression( void abstract_environmentt::erase(const symbol_exprt &expr) { - map.erase_if_exists(expr.get_identifier()); + map.erase_if_exists(expr.identifier()); } std::vector diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp index 3706931aba1..76fb1a6d7b7 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp @@ -159,7 +159,7 @@ void constant_pointer_abstract_objectt::output( { const symbol_exprt &symbol_pointed_to(to_symbol_expr(addressee)); - out << symbol_pointed_to.get_identifier(); + out << symbol_pointed_to.identifier(); } else if(addressee.id() == ID_dynamic_object) { @@ -172,7 +172,7 @@ void constant_pointer_abstract_objectt::output( if(array.id() == ID_symbol) { auto const &array_symbol = to_symbol_expr(array); - out << array_symbol.get_identifier() << "["; + out << array_symbol.identifier() << "["; if(array_index.index().is_constant()) out << to_constant_expr(array_index.index()).get_value(); else @@ -340,8 +340,8 @@ exprt symbol_ptr_comparison_expr( exprt const &lhs, exprt const &rhs) { - auto const &lhs_identifier = to_symbol_expr(lhs).get_identifier(); - auto const &rhs_identifier = to_symbol_expr(rhs).get_identifier(); + auto const &lhs_identifier = to_symbol_expr(lhs).identifier(); + auto const &rhs_identifier = to_symbol_expr(rhs).identifier(); if(id == ID_equal) return to_bool_expr(lhs_identifier == rhs_identifier); diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index b348096522c..10efb04e147 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -291,7 +291,7 @@ void variable_sensitivity_domaint::transform_function_call( { // called function identifier const symbol_exprt &symbol_expr = to_symbol_expr(function); - const irep_idt function_id = symbol_expr.get_identifier(); + const irep_idt function_id = symbol_expr.identifier(); const code_function_callt::argumentst &called_arguments = from->call_arguments(); diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index de4db8e8ef5..eaa4d5b25fe 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -739,7 +739,7 @@ void c_typecheck_baset::check_history_expr_return_value( if(!can_cast_expr(expr)) return false; - return to_symbol_expr(expr).get_identifier() == id; + return to_symbol_expr(expr).identifier() == id; }; if(!has_subexpr(expr, pred)) @@ -760,7 +760,7 @@ void c_typecheck_baset::check_was_freed( if(!can_cast_expr(expr)) return false; - return to_symbol_expr(expr).get_identifier() == id; + return to_symbol_expr(expr).identifier() == id; }; if(has_subexpr(expr, pred)) @@ -963,7 +963,7 @@ void c_typecheck_baset::typecheck_declaration( } for(const auto ¶meter_sym : temporary_parameter_symbols) - parameter_map.erase(parameter_sym.get_identifier()); + parameter_map.erase(parameter_sym.identifier()); // create a contract symbol symbolt contract; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 9b2e3723627..3954d80f21d 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -1026,7 +1026,7 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) { throw invalid_source_file_exceptiont( "expecting void return type for function '" + - id2string(to_symbol_expr(funcall.function()).get_identifier()) + + id2string(to_symbol_expr(funcall.function()).identifier()) + "' called in assigns clause", target.source_location()); } @@ -1071,7 +1071,7 @@ void c_typecheck_baset::typecheck_spec_frees_target(exprt &target) { throw invalid_source_file_exceptiont( "expecting void return type for function '" + - id2string(to_symbol_expr(funcall.function()).get_identifier()) + + id2string(to_symbol_expr(funcall.function()).identifier()) + "' called in frees clause", target.source_location()); } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index d2219a7a29a..c8e7e413e00 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -845,7 +845,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) { - irep_idt identifier=to_symbol_expr(expr).get_identifier(); + irep_idt identifier = to_symbol_expr(expr).identifier(); // Is it a parameter? We do this while checking parameter lists. id_type_mapt::const_iterator p_it=parameter_map.find(identifier); @@ -863,7 +863,7 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr) if(entry!=asm_label_map.end()) { identifier=entry->second; - to_symbol_expr(expr).set_identifier(identifier); + to_symbol_expr(expr).identifier(identifier); } // look it up @@ -2006,7 +2006,7 @@ void c_typecheck_baset::typecheck_typed_target_call( { INVARIANT( expr.function().id() == ID_symbol && - to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX + to_symbol_expr(expr.function()).identifier() == CPROVER_PREFIX "typed_target", "expression must be a " CPROVER_PREFIX "typed_target function call"); @@ -2040,7 +2040,7 @@ void c_typecheck_baset::typecheck_typed_target_call( } // rewrite call to "assignable" - f_op.set_identifier(CPROVER_PREFIX "assignable"); + f_op.identifier(CPROVER_PREFIX "assignable"); exprt::operandst arguments; // pointer arguments.push_back(address_of_exprt(arg0)); @@ -2061,7 +2061,7 @@ void c_typecheck_baset::typecheck_obeys_contract_call( { INVARIANT( expr.function().id() == ID_symbol && - to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX + to_symbol_expr(expr.function()).identifier() == CPROVER_PREFIX "obeys_contract", "expression must be a " CPROVER_PREFIX "obeys_contract function call"); @@ -2148,7 +2148,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(f_op.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(f_op).get_identifier(); + irep_idt identifier = to_symbol_expr(f_op).identifier(); asm_label_mapt::const_iterator entry= asm_label_map.find(identifier); @@ -2401,8 +2401,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( else if( auto shadow_memory_builtin = typecheck_shadow_memory_builtin(expr)) { - irep_idt shadow_memory_builtin_id = - shadow_memory_builtin->get_identifier(); + irep_idt shadow_memory_builtin_id = shadow_memory_builtin->identifier(); const auto builtin_code_type = to_code_type(shadow_memory_builtin->type()); @@ -2434,7 +2433,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin( identifier, expr.arguments(), f_op.source_location())) { - irep_idt identifier_with_type = gcc_polymorphic->get_identifier(); + irep_idt identifier_with_type = gcc_polymorphic->identifier(); auto ¶meters = to_code_type(gcc_polymorphic->type()).parameters(); INVARIANT( !parameters.empty(), @@ -2456,7 +2455,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call( id2string(identifier) + "_" + type_to_partial_identifier(parameters.front().type(), *this); } - gcc_polymorphic->set_identifier(identifier_with_type); + gcc_polymorphic->identifier(identifier_with_type); if(!symbol_table.has_symbol(identifier_with_type)) { @@ -2633,7 +2632,7 @@ exprt c_typecheck_baset::do_special_functions( if(f_op.id()!=ID_symbol) return nil_exprt(); - const irep_idt &identifier=to_symbol_expr(f_op).get_identifier(); + const irep_idt &identifier = to_symbol_expr(f_op).identifier(); if(identifier == CPROVER_PREFIX "pointer_equals") { @@ -3869,7 +3868,7 @@ exprt c_typecheck_baset::typecheck_builtin_overflow( side_effect_expr_function_callt &expr, const irep_idt &arith_op) { - const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr.function()).identifier(); // check function signature if(expr.arguments().size() != 3) @@ -3931,7 +3930,7 @@ exprt c_typecheck_baset::typecheck_builtin_overflow( exprt c_typecheck_baset::typecheck_saturating_arithmetic( const side_effect_expr_function_callt &expr) { - const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr.function()).identifier(); // check function signature if(expr.arguments().size() != 2) @@ -4751,7 +4750,7 @@ class is_compile_time_constantt if(e.id() == ID_symbol) { return e.type().id() == ID_code || - ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime; + ns.lookup(to_symbol_expr(e).identifier()).is_static_lifetime; } else if(e.id() == ID_array && e.get_bool(ID_C_string_constant)) return true; diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index 5632868d13a..dd56ef7b239 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -1239,7 +1239,7 @@ code_blockt c_typecheck_baset::instantiate_gcc_polymorphic_builtin( const irep_idt &identifier, const symbol_exprt &function_symbol) { - const irep_idt &identifier_with_type = function_symbol.get_identifier(); + const irep_idt &identifier_with_type = function_symbol.identifier(); const code_typet &code_type = to_code_type(function_symbol.type()); const source_locationt &source_location = function_symbol.source_location(); @@ -1405,7 +1405,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector( { const exprt &f_op = expr.function(); const source_locationt &source_location = expr.source_location(); - const irep_idt &identifier = to_symbol_expr(f_op).get_identifier(); + const irep_idt &identifier = to_symbol_expr(f_op).identifier(); exprt::operandst arguments = expr.arguments(); diff --git a/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp b/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp index 26667aca9df..7c6ee139a76 100644 --- a/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp +++ b/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp @@ -230,7 +230,7 @@ std::optional c_typecheck_baset::typecheck_shadow_memory_builtin( INVARIANT( can_cast_expr(f_op), "expr.function() has to be a symbol_expr"); - const irep_idt &identifier = to_symbol_expr(f_op).get_identifier(); + const irep_idt &identifier = to_symbol_expr(f_op).identifier(); if( identifier == CPROVER_PREFIX "field_decl_global" || diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c7e38d5c8c6..02e8222b964 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2862,7 +2862,7 @@ expr2ct::convert_code_frontend_decl(const codet &src, unsigned indent) std::string dest=indent_str(indent); const symbolt *symbol=nullptr; - if(!ns.lookup(to_symbol_expr(src.op0()).get_identifier(), symbol)) + if(!ns.lookup(to_symbol_expr(src.op0()).identifier(), symbol)) { if(symbol->is_file_local && (src.op0().type().id()==ID_code || symbol->is_static_lifetime)) diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index 951a9dbb453..3a825087932 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -36,7 +36,7 @@ void goto_convertt::do_prob_uniform( const exprt::operandst &arguments, goto_programt &dest) { - const irep_idt &identifier = function.get_identifier(); + const irep_idt &identifier = function.identifier(); // make it a side effect if there is an LHS if(arguments.size() != 2) @@ -113,7 +113,7 @@ void goto_convertt::do_prob_coin( const exprt::operandst &arguments, goto_programt &dest) { - const irep_idt &identifier = function.get_identifier(); + const irep_idt &identifier = function.identifier(); // make it a side effect if there is an LHS if(arguments.size() != 2) @@ -196,7 +196,7 @@ void goto_convertt::do_printf( const exprt::operandst &arguments, goto_programt &dest) { - const irep_idt &f_id = function.get_identifier(); + const irep_idt &f_id = function.identifier(); PRECONDITION(f_id == CPROVER_PREFIX "printf"); @@ -210,7 +210,7 @@ void goto_convertt::do_scanf( const exprt::operandst &arguments, goto_programt &dest) { - const irep_idt &f_id = function.get_identifier(); + const irep_idt &f_id = function.identifier(); if(f_id == CPROVER_PREFIX "scanf") { @@ -496,7 +496,7 @@ void goto_convertt::do_cpp_new( typecast_exprt(tmp_symbol_expr, lhs.type()), rhs.find_source_location())); - side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).identifier()); destruct_locals(side_effects.temporaries, dest, ns); // grab initializer @@ -794,7 +794,7 @@ void goto_convertt::do_alloca( this_alloca_ptr, std::move(rhs), source_location)); if(lhs.is_nil()) - destruct_locals({to_symbol_expr(new_lhs).get_identifier()}, dest, ns); + destruct_locals({to_symbol_expr(new_lhs).identifier()}, dest, ns); // mark pointer to alloca result as dead, unless the alloca result (in // this_alloca_ptr) is still NULL @@ -829,7 +829,7 @@ void goto_convertt::do_function_call_symbol( return; // ignore // lookup symbol - const irep_idt &identifier = function.get_identifier(); + const irep_idt &identifier = function.identifier(); const symbolt *symbol; if(ns.lookup(identifier, symbol)) @@ -1134,7 +1134,7 @@ void goto_convertt::do_function_call_symbol( mathematical_function_typet function_type{ domain, function_call_type.return_type()}; const function_application_exprt rhs( - symbol_exprt{function.get_identifier(), function_type}, arguments); + symbol_exprt{function.identifier(), function_type}, arguments); code_assignt assignment(lhs, rhs); assignment.add_source_location() = function.source_location(); @@ -1486,7 +1486,7 @@ void goto_convertt::do_function_call_symbol( "builtin declaration should match constructed type"); symbol_exprt new_function = function; - new_function.set_identifier(name); + new_function.identifier(name); new_function.type() = f_type; code_function_callt function_call(lhs, new_function, new_arguments); diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 68c04604a94..ad0419853a9 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -444,9 +444,8 @@ void goto_check_ct::collect_allocations(const goto_functionst &goto_functions) const auto &function = instruction.call_function(); if( - function.id() != ID_symbol || - to_symbol_expr(function).get_identifier() != CPROVER_PREFIX - "allocated_memory") + function.id() != ID_symbol || to_symbol_expr(function).identifier() != + CPROVER_PREFIX "allocated_memory") continue; const code_function_callt::argumentst &args = @@ -474,7 +473,7 @@ void goto_check_ct::invalidate(const exprt &lhs) else if(lhs.id() == ID_symbol) { // clear all assertions about 'symbol' - const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier(); + const irep_idt &lhs_id = to_symbol_expr(lhs).identifier(); for(auto it = assertions.begin(); it != assertions.end();) { @@ -1509,7 +1508,7 @@ void goto_check_ct::pointer_primitive_check( { const auto &symbol_expr = to_symbol_expr(pointer); - if(symbol_expr.get_identifier().starts_with(CPROVER_PREFIX)) + if(symbol_expr.identifier().starts_with(CPROVER_PREFIX)) return; } @@ -2333,8 +2332,7 @@ void goto_check_ct::check_shadow_memory_api_calls( if(i.call_function().id() != ID_symbol) return; - const irep_idt &identifier = - to_symbol_expr(i.call_function()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(i.call_function()).identifier(); if( identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 5cb721e8734..72217bac88a 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -577,7 +577,7 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr( side_effects.temporaries.clear(); if(expr.is_not_nil()) - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); return side_effects; } diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 60674e6e430..4ef706f24dd 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -1416,7 +1416,7 @@ void goto_convertt::convert_switch( convert(copy_value, side_effects.side_effects, mode); argument = new_symbol.symbol_expr(); - side_effects.add_temporary(to_symbol_expr(argument).get_identifier()); + side_effects.add_temporary(to_symbol_expr(argument).identifier()); } // save break/default/cases targets @@ -2183,7 +2183,7 @@ irep_idt goto_convertt::make_temp_symbol( expr = new_symbol.symbol_expr(); - return to_symbol_expr(expr).get_identifier(); + return to_symbol_expr(expr).identifier(); } void goto_convert( diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index 28943332d12..3282bd6dbfc 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -380,8 +380,7 @@ goto_convertt::clean_expr_resultt goto_convertt::remove_function_call( if(expr.function().id() == ID_symbol) { - const irep_idt &identifier = - to_symbol_expr(expr.function()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr.function()).identifier(); const symbolt &symbol = ns.lookup(identifier); new_base_name += '_'; @@ -411,7 +410,7 @@ goto_convertt::clean_expr_resultt goto_convertt::remove_function_call( static_cast(expr) = new_symbol.symbol_expr(); - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); return side_effects; } @@ -449,7 +448,7 @@ goto_convertt::remove_cpp_new(side_effect_exprt &expr, bool result_is_used) if(result_is_used) { static_cast(expr) = new_symbol.symbol_expr(); - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); } else expr.make_nil(); @@ -503,7 +502,7 @@ goto_convertt::clean_expr_resultt goto_convertt::remove_malloc( convert(call, side_effects.side_effects, mode); - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); } else convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode); @@ -551,7 +550,7 @@ goto_convertt::remove_temporary_object(side_effect_exprt &expr) static_cast(expr) = new_symbol.symbol_expr(); - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); return side_effects; } @@ -625,7 +624,7 @@ goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression( static_cast(expr) = tmp_symbol_expr; - side_effects.add_temporary(to_symbol_expr(expr).get_identifier()); + side_effects.add_temporary(to_symbol_expr(expr).identifier()); return side_effects; } diff --git a/src/ansi-c/goto-conversion/scope_tree.h b/src/ansi-c/goto-conversion/scope_tree.h index 329e46c0578..6a76d72986a 100644 --- a/src/ansi-c/goto-conversion/scope_tree.h +++ b/src/ansi-c/goto-conversion/scope_tree.h @@ -189,8 +189,7 @@ class scope_treet if(!declaration.has_value()) return ""; - return id2string( - declaration->instruction->decl_symbol().get_identifier()); + return id2string(declaration->instruction->decl_symbol().identifier()); } }; diff --git a/src/ansi-c/goto-conversion/string_instrumentation.cpp b/src/ansi-c/goto-conversion/string_instrumentation.cpp index df9ca3a147b..598fe4574e0 100644 --- a/src/ansi-c/goto-conversion/string_instrumentation.cpp +++ b/src/ansi-c/goto-conversion/string_instrumentation.cpp @@ -206,7 +206,7 @@ void string_instrumentationt::do_function_call( if(function.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); if(identifier == "strcoll") { diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 6e852100532..bc058d4fb03 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -168,7 +168,7 @@ static std::string type2name( const exprt &size = to_array_type(type).size(); if(size.id() == ID_symbol) - result += "ARR" + id2string(to_symbol_expr(size).get_identifier()); + result += "ARR" + id2string(to_symbol_expr(size).identifier()); else { const auto size_int = numeric_cast(size); diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index c773b91108f..71821c14941 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -56,7 +56,7 @@ std::string cpp_typecheckt::template_suffix( if(e.id() == ID_symbol) { const symbol_exprt &s = to_symbol_expr(e); - const symbolt &symbol = lookup(s.get_identifier()); + const symbolt &symbol = lookup(s.identifier()); if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant)) e = symbol.value; diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index d358bf61680..48c62767aae 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -774,7 +774,7 @@ void cpp_typecheckt::check_fixed_size_array(typet &type) if(array_type.size().id() == ID_symbol) { const symbol_exprt &s = to_symbol_expr(array_type.size()); - const symbolt &symbol = lookup(s.get_identifier()); + const symbolt &symbol = lookup(s.identifier()); if(cpp_is_pod(symbol.type) && symbol.type.get_bool(ID_C_constant)) array_type.size() = symbol.value; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 2685771889c..b162bb60889 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1170,7 +1170,7 @@ void cpp_typecheckt::typecheck_expr_member( { // it must be a static component const struct_typet::componentt &pcomp = - type.get_component(to_symbol_expr(symbol_expr).get_identifier()); + type.get_component(to_symbol_expr(symbol_expr).identifier()); if(pcomp.is_nil()) { diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index e555353ed55..fb8d19068f4 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -167,7 +167,7 @@ void cpp_typecheck_resolvet::remove_duplicates( irep_idt id; if(old_id.id() == ID_symbol) - id = to_symbol_expr(old_id).get_identifier(); + id = to_symbol_expr(old_id).identifier(); else if(old_id.id() == ID_type && old_id.type().id() == ID_struct_tag) id = to_struct_tag_type(old_id.type()).get_identifier(); else if(old_id.id() == ID_type && old_id.type().id() == ID_union_tag) @@ -1066,7 +1066,7 @@ struct_tag_typet cpp_typecheck_resolvet::disambiguate_template_classes( if(arg.id() == ID_symbol) { const symbol_exprt &s = to_symbol_expr(arg); - const symbolt &symbol = cpp_typecheck.lookup(s.get_identifier()); + const symbolt &symbol = cpp_typecheck.lookup(s.identifier()); if( cpp_typecheck.cpp_is_pod(symbol.type) && @@ -1919,8 +1919,7 @@ exprt cpp_typecheck_resolvet::guess_function_template_args( // We need to guess in the case of function templates! - irep_idt template_identifier= - to_symbol_expr(expr).get_identifier(); + irep_idt template_identifier = to_symbol_expr(expr).identifier(); const symbolt &template_symbol= cpp_typecheck.lookup(template_identifier); @@ -2041,7 +2040,7 @@ void cpp_typecheck_resolvet::apply_template_args( return; // templates are always symbols const symbolt &template_symbol = - cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier()); + cpp_typecheck.lookup(to_symbol_expr(expr).identifier()); if(!template_symbol.type.get_bool(ID_is_template)) return; diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp index 566db7156eb..16767e6e5a3 100644 --- a/src/cpp/template_map.cpp +++ b/src/cpp/template_map.cpp @@ -77,7 +77,7 @@ void template_mapt::apply(exprt &expr) const if(expr.id()==ID_symbol) { expr_mapt::const_iterator m_it = - expr_map.find(to_symbol_expr(expr).get_identifier()); + expr_map.find(to_symbol_expr(expr).identifier()); if(m_it!=expr_map.end()) { diff --git a/src/cprover/axioms.cpp b/src/cprover/axioms.cpp index 6b002370ebc..e381f17abbb 100644 --- a/src/cprover/axioms.cpp +++ b/src/cprover/axioms.cpp @@ -329,7 +329,7 @@ void axiomst::initial_state() for(const auto &object : address_taken) { const symbolt *symbol; - if(ns.lookup(object.get_identifier(), symbol)) + if(ns.lookup(object.identifier(), symbol)) continue; if(symbol->is_static_lifetime || !symbol->is_lvalue) diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index 9197306f0b1..bb9e01dc6de 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -304,7 +304,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr) if(expr.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(expr).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr).identifier(); return map.get_literals(identifier, type, bits); } diff --git a/src/cprover/c_safety_checks.cpp b/src/cprover/c_safety_checks.cpp index 98a4f67611a..2c4850f760f 100644 --- a/src/cprover/c_safety_checks.cpp +++ b/src/cprover/c_safety_checks.cpp @@ -271,7 +271,7 @@ void c_safety_checks( const auto &function = it->call_function(); if(function.id() == ID_symbol) { - const auto &identifier = to_symbol_expr(function).get_identifier(); + const auto &identifier = to_symbol_expr(function).identifier(); if(identifier == "free") { if( diff --git a/src/cprover/equality_propagation.cpp b/src/cprover/equality_propagation.cpp index 41874eb08ad..8eb8125f001 100644 --- a/src/cprover/equality_propagation.cpp +++ b/src/cprover/equality_propagation.cpp @@ -40,7 +40,7 @@ void equality_propagation(std::vector &constraints) const auto &symbol_expr = to_symbol_expr(equal_expr.lhs()); // this is a (deliberate) no-op when the symbol is already in the map auto insert_result = - values.insert({symbol_expr.get_identifier(), equal_expr.rhs()}); + values.insert({symbol_expr.identifier(), equal_expr.rhs()}); if(insert_result.second) { // insertion has happened diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp index 7440a7a0153..e386f98512d 100644 --- a/src/cprover/instrument_contracts.cpp +++ b/src/cprover/instrument_contracts.cpp @@ -190,7 +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 symbol_expr.get_identifier().starts_with( + return symbol_expr.identifier().starts_with( id2string(function_identifier) + "::"); } else @@ -202,7 +202,7 @@ static bool is_old(const exprt &lhs) if(lhs.id() == ID_symbol) { const auto &symbol_expr = to_symbol_expr(lhs); - return symbol_expr.get_identifier().starts_with("old::"); + return symbol_expr.identifier().starts_with("old::"); } else return false; diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp index 036ace61a22..8d4a5e9c587 100644 --- a/src/cprover/may_alias.cpp +++ b/src/cprover/may_alias.cpp @@ -113,7 +113,7 @@ bool stack_and_not_dirty( if(object.has_value()) { auto symbol_expr = object->object_expr(); - auto identifier = symbol_expr.get_identifier(); + auto identifier = symbol_expr.identifier(); if(identifier.starts_with("va_arg::")) return true; // on the stack, and might alias else if(identifier.starts_with("var_args::")) diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 3ebd8f42f41..39e89cb0d45 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -216,7 +216,7 @@ exprt state_encodingt::evaluate_expr_rec( { const auto &symbol_expr = to_symbol_expr(what); - if(symbol_expr.get_identifier() == CPROVER_PREFIX "return_value") + if(symbol_expr.identifier() == CPROVER_PREFIX "return_value") { auto new_symbol = symbol_exprt("return_value", what.type()); return evaluate_exprt( @@ -650,7 +650,7 @@ void state_encodingt::function_call_symbol( { const auto &function = to_symbol_expr(loc->call_function()); const auto &type = to_code_type(function.type()); - auto identifier = function.get_identifier(); + auto identifier = function.identifier(); auto new_annotation = annotation + u8" \u2192 " + id2string(identifier); dest.annotation(new_annotation); @@ -980,15 +980,15 @@ void state_encodingt::encode( if( lhs.id() == ID_symbol && has_prefix( - id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX) && - to_symbol_expr(lhs).get_identifier() != CPROVER_PREFIX "rounding_mode") + id2string(to_symbol_expr(lhs).identifier()), CPROVER_PREFIX) && + to_symbol_expr(lhs).identifier() != CPROVER_PREFIX "rounding_mode") { // skip for now dest << equal_exprt(out_state_expr(loc), in_state_expr(loc)); } else if( lhs.id() == ID_symbol && - to_symbol_expr(lhs).get_identifier() == "_DefaultRuneLocale") + to_symbol_expr(lhs).identifier() == "_DefaultRuneLocale") { // /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/runetype.h // skip for now diff --git a/src/cprover/variable_encoding.cpp b/src/cprover/variable_encoding.cpp index 54b2a372efd..c4e5489a96d 100644 --- a/src/cprover/variable_encoding.cpp +++ b/src/cprover/variable_encoding.cpp @@ -115,9 +115,8 @@ void variable_encoding(std::vector &constraints) std::sort( variables.begin(), variables.end(), - [](const symbol_exprt &a, const symbol_exprt &b) { - return id2string(a.get_identifier()) < id2string(b.get_identifier()); - }); + [](const symbol_exprt &a, const symbol_exprt &b) + { return id2string(a.identifier()) < id2string(b.identifier()); }); for(auto &c : constraints) c = variable_encoding(c, variables); diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 33da2e6640f..a4e0615f324 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -80,7 +80,7 @@ void taint_analysist::instrument( if(function.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); std::set identifiers; diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 465784cde10..12319f59021 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -232,7 +232,7 @@ int linker_script_merget::pointerize_linker_defined_symbols( ret=1; for(const auto &sym : to_pointerize) { - log.error() << " Could not pointerize '" << sym.get_identifier() + log.error() << " Could not pointerize '" << sym.identifier() << "' in symbol table entry " << it->first << ". Pretty:\n" << sym.pretty() << "\n"; } @@ -263,7 +263,7 @@ int linker_script_merget::pointerize_linker_defined_symbols( ret=1; for(const auto &sym : to_pointerize) { - log.error() << " Could not pointerize '" << sym.get_identifier() + log.error() << " Could not pointerize '" << sym.identifier() << "' in function " << gf.first << ". Pretty:\n" << sym.pretty() << "\n"; log.error().source_location = instruction.source_location(); @@ -310,7 +310,7 @@ int linker_script_merget::pointerize_subexprs_of( continue; // take a copy, expr will be changed below const symbol_exprt inner_symbol=pattern.inner_symbol(expr); - if(pair.first!=inner_symbol.get_identifier()) + if(pair.first != inner_symbol.identifier()) continue; tmp=replace_expr(expr, linker_values, inner_symbol, pair.first, pattern.description()); @@ -320,7 +320,7 @@ int linker_script_merget::pointerize_subexprs_of( if(result==to_pointerize.end()) { fail=1; - log.error() << "Too many removals of '" << inner_symbol.get_identifier() + log.error() << "Too many removals of '" << inner_symbol.identifier() << "'" << messaget::eom; } else @@ -350,7 +350,7 @@ void linker_script_merget::symbols_to_pointerize( if(op.id()!=ID_symbol) continue; const symbol_exprt &sym_exp=to_symbol_expr(op); - const auto &pair=linker_values.find(sym_exp.get_identifier()); + const auto &pair = linker_values.find(sym_exp.identifier()); if(pair!=linker_values.end()) to_pointerize.push_back(sym_exp); } diff --git a/src/goto-checker/fatal_assertions.cpp b/src/goto-checker/fatal_assertions.cpp index 0891c77fbb2..ddc9e3af869 100644 --- a/src/goto-checker/fatal_assertions.cpp +++ b/src/goto-checker/fatal_assertions.cpp @@ -85,7 +85,7 @@ reachable_fixpoint(const loc_sett &locs, const goto_functionst &goto_functions) if(function.id() == ID_symbol) { // add the callee to the working set - auto &function_identifier = to_symbol_expr(function).get_identifier(); + auto &function_identifier = to_symbol_expr(function).identifier(); auto function_iterator = goto_functions.function_map.find(function_identifier); CHECK_RETURN(function_iterator != goto_functions.function_map.end()); diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 8706e406c80..93810d52787 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -476,7 +476,7 @@ function_call_harness_generatort::implt::declare_arguments( auto argument = allocate_objects.allocate_automatic_local_object( remove_const(parameter.type()), parameter.get_base_name()); parameter_name_to_argument_name.insert( - {parameter.get_base_name(), argument.get_identifier()}); + {parameter.get_base_name(), argument.identifier()}); arguments.push_back(argument); } diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 52a51fc2560..4e2f94e868b 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -281,7 +281,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort void collect_references(const exprt &expr, Adder &&add_reference) const { if(expr.id() == ID_symbol) - add_reference(to_symbol_expr(expr).get_identifier()); + add_reference(to_symbol_expr(expr).identifier()); for(const auto &operand : expr.operands()) { collect_references(operand, add_reference); diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 395808b746b..a2f566db749 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -142,7 +142,7 @@ void recursive_initializationt::initialize( { if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty()) { - auto lhs_id = to_symbol_expr(lhs).get_identifier(); + auto lhs_id = to_symbol_expr(lhs).identifier(); for(const auto &selection_spec : initialization_config.selection_specs) { if(selection_spec.front() == lhs_id) @@ -158,7 +158,7 @@ void recursive_initializationt::initialize( if(lhs.id() == ID_symbol) { const auto maybe_cluster_index = - find_equal_cluster(to_symbol_expr(lhs).get_identifier()); + find_equal_cluster(to_symbol_expr(lhs).identifier()); if(maybe_cluster_index.has_value()) { if(common_arguments_origins[*maybe_cluster_index].has_value()) @@ -196,7 +196,7 @@ void recursive_initializationt::initialize( if(lhs.id() == ID_symbol) { - const irep_idt &lhs_name = to_symbol_expr(lhs).get_identifier(); + const irep_idt &lhs_name = to_symbol_expr(lhs).identifier(); if(should_be_treated_as_array(lhs_name)) { auto size_var = get_associated_size_variable(lhs_name); @@ -303,7 +303,7 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) bool has_size_param = false; if(expr.id() == ID_symbol) { - expr_name = to_symbol_expr(expr).get_identifier(); + expr_name = to_symbol_expr(expr).identifier(); is_nullable = initialization_config.potential_null_function_pointers.count( expr_name.value()); if(should_be_treated_as_array(*expr_name)) @@ -906,9 +906,8 @@ bool recursive_initializationt::needs_freeing(const exprt &expr) const { if(common_arguments_origin.has_value() && expr.id() == ID_symbol) { - auto origin_name = - to_symbol_expr(*common_arguments_origin).get_identifier(); - auto expr_name = to_symbol_expr(expr).get_identifier(); + auto origin_name = to_symbol_expr(*common_arguments_origin).identifier(); + auto expr_name = to_symbol_expr(expr).identifier(); return origin_name == expr_name; } } @@ -938,7 +937,7 @@ void recursive_initializationt::free_if_possible( code_blockt &body) { PRECONDITION(expr.id() == ID_symbol); - const auto expr_id = to_symbol_expr(expr).get_identifier(); + const auto expr_id = to_symbol_expr(expr).identifier(); const auto maybe_cluster_index = find_equal_cluster(expr_id); if(!maybe_cluster_index.has_value()) { @@ -949,7 +948,7 @@ void recursive_initializationt::free_if_possible( if( to_symbol_expr(*common_arguments_origins[*maybe_cluster_index]) - .get_identifier() != expr_id && + .identifier() != expr_id && initialization_config.arguments_may_be_equal) { // in equality cluster but not common origin -> free if not equal to origin @@ -1013,7 +1012,7 @@ code_blockt recursive_initializationt::build_function_pointer_constructor( // This is either address of or pointer; in pointer case, we don't // need to do anything. In the address of case, the operand is // a symbol representing a target function. - to_symbol_expr(to_address_of_expr(target).object()).get_identifier() + to_symbol_expr(to_address_of_expr(target).object()).identifier() : ""; // skip referencing globals because the corresponding symbols in the symbol // table are no longer marked as file local. diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index c4ecf3063b9..0f009878df5 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -415,7 +415,7 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator) { if(it->id()==ID_symbol && it->type() == bool_typet()) { - const irep_idt &id=to_symbol_expr(*it).get_identifier(); + const irep_idt &id = to_symbol_expr(*it).identifier(); const symbolt &sym = symbol_table.lookup_ref(id); if(sym.module=="scratch") diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 40d5c667c8b..765ac523b5c 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -50,8 +50,8 @@ void show_call_sequences( const exprt &callee = t->call_function(); if(callee.id()==ID_symbol) { - std::cout << caller << " -> " - << to_symbol_expr(callee).get_identifier() << '\n'; + std::cout << caller << " -> " << to_symbol_expr(callee).identifier() + << '\n'; } } @@ -202,7 +202,7 @@ void check_call_sequencet::operator()() const exprt &function = e.pc->call_function(); if(function.id()==ID_symbol) { - irep_idt identifier=to_symbol_expr(function).get_identifier(); + irep_idt identifier = to_symbol_expr(function).identifier(); if(sequence[e.index]==identifier) { @@ -282,7 +282,7 @@ static void list_calls_and_arguments( if(f.id()!=ID_symbol) continue; - const irep_idt &identifier=to_symbol_expr(f).get_identifier(); + const irep_idt &identifier = to_symbol_expr(f).identifier(); if(identifier == INITIALIZE_FUNCTION) continue; diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-instrument/concurrency.cpp index 90daf39c4a0..45d7bcf327d 100644 --- a/src/goto-instrument/concurrency.cpp +++ b/src/goto-instrument/concurrency.cpp @@ -81,7 +81,7 @@ void concurrency_instrumentationt::instrument(exprt &expr) for(const symbol_exprt &s : find_symbols(expr)) { - shared_varst::const_iterator v_it = shared_vars.find(s.get_identifier()); + shared_varst::const_iterator v_it = shared_vars.find(s.identifier()); if(v_it != shared_vars.end()) { diff --git a/src/goto-instrument/contracts/cfg_info.h b/src/goto-instrument/contracts/cfg_info.h index 42c2c35a127..3fd7db72ca7 100644 --- a/src/goto-instrument/contracts/cfg_info.h +++ b/src/goto-instrument/contracts/cfg_info.h @@ -53,7 +53,7 @@ class cfg_infot // case-splitting on the lhs structure copied from symex_assignt::assign_rec if(expr.id() == ID_symbol) { - return is_local(to_symbol_expr(expr).get_identifier()); + return is_local(to_symbol_expr(expr).identifier()); } else if(expr.id() == ID_index) { @@ -148,7 +148,7 @@ class loop_cfg_infot : public cfg_infot for(const auto &t : loop) { if(t->is_decl()) - locals.insert(t->decl_symbol().get_identifier()); + locals.insert(t->decl_symbol().identifier()); } } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 046bc714e97..38a5322f219 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -536,7 +536,7 @@ static void throw_on_unsupported(const goto_programt &program) { if( it.is_function_call() && it.call_function().id() == ID_symbol && - to_symbol_expr(it.call_function()).get_identifier() == CPROVER_PREFIX + to_symbol_expr(it.call_function()).identifier() == CPROVER_PREFIX "obeys_contract") { throw invalid_source_file_exceptiont( @@ -609,7 +609,7 @@ void code_contractst::apply_function_contract( PRECONDITION(const_target->call_function().id() == ID_symbol); const irep_idt &target_function = - to_symbol_expr(const_target->call_function()).get_identifier(); + to_symbol_expr(const_target->call_function()).identifier(); const symbolt &function_symbol = ns.lookup(target_function); const code_typet &function_type = to_code_type(function_symbol.type); @@ -1445,7 +1445,7 @@ void code_contractst::replace_calls(const std::set &to_replace) continue; const irep_idt &called_function = - to_symbol_expr(ins->call_function()).get_identifier(); + to_symbol_expr(ins->call_function()).identifier(); auto found = std::find( to_replace.begin(), to_replace.end(), id2string(called_function)); if(found == to_replace.end()) @@ -1514,7 +1514,7 @@ void code_contractst::apply_loop_contracts( const auto &assign_lhs = expr_try_dynamic_cast(it_instr->assign_lhs()); original_loop_number_map[it_instr] = get_suffix_unsigned( - id2string(assign_lhs->get_identifier()), + id2string(assign_lhs->identifier()), std::string(ENTERED_LOOP) + "__"); continue; } @@ -1531,7 +1531,7 @@ void code_contractst::apply_loop_contracts( const auto &assign_lhs = expr_try_dynamic_cast(it_instr->assign_lhs()); loop_number_of_loop_havoc = get_suffix_unsigned( - id2string(assign_lhs->get_identifier()), + id2string(assign_lhs->identifier()), std::string(IN_LOOP_HAVOC_BLOCK) + "__"); continue; } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index dc8cffb044b..af61dac31ed 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -235,8 +235,7 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns) { if( root_object.id() == ID_symbol && - expr_try_dynamic_cast(root_object)->get_identifier() == - ident) + expr_try_dynamic_cast(root_object)->identifier() == ident) { return true; } @@ -596,7 +595,7 @@ dfcc_cfg_infot::dfcc_cfg_infot( target++) { if(target->is_decl() && dfcc_is_loop_top_level(target)) - top_level_local.insert(target->decl_symbol().get_identifier()); + top_level_local.insert(target->decl_symbol().identifier()); } top_level_tracked = @@ -773,8 +772,8 @@ bool dfcc_cfg_infot::must_track_decl_or_dead( goto_programt::const_targett target) const { PRECONDITION(target->is_decl() || target->is_dead()); - auto &ident = target->is_decl() ? target->decl_symbol().get_identifier() - : target->dead_symbol().get_identifier(); + auto &ident = target->is_decl() ? target->decl_symbol().identifier() + : target->dead_symbol().identifier(); auto &tracked = get_tracked_set(target); return tracked.find(ident) != tracked.end(); } @@ -805,7 +804,7 @@ static bool must_check_lhs_from_local_and_tracked( // non-tracked identifiers the check will fail but this is sound anyway. return true; } - const auto &id = to_symbol_expr(expr).get_identifier(); + const auto &id = to_symbol_expr(expr).identifier(); if(dfcc_is_cprover_static_symbol(id)) { // Skip the check if we have a single cprover symbol as root object diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp index 0e02823c4d8..caf87eb62fa 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp @@ -74,12 +74,12 @@ std::unordered_set gen_loop_locals_set( // All variables declared in loops are loop locals. if(i_it->is_decl() && loop.contains(i_it)) { - loop_locals.insert(i_it->decl_symbol().get_identifier()); + loop_locals.insert(i_it->decl_symbol().identifier()); } // Record all other declared variables and their ranges. else if(i_it->is_decl()) { - non_loop_decls.insert(i_it->decl_symbol().get_identifier()); + non_loop_decls.insert(i_it->decl_symbol().identifier()); } // Record all writing/reading outside the loop. else if( @@ -288,7 +288,7 @@ static void remove_dead_object_assignment(goto_functiont &goto_function) if( lhs.id() == ID_symbol && - to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object") + to_symbol_expr(lhs).identifier() == CPROVER_PREFIX "dead_object") { i_it->turn_into_skip(); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index e469620c23f..1979cdc8a88 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -850,7 +850,7 @@ void dfcc_instrumentt::instrument_call_instruction( { // this is a function call if(!do_not_instrument( - to_symbol_expr(target->call_function()).get_identifier())) + to_symbol_expr(target->call_function()).identifier())) { // pass write set argument only if function is known to be instrumented target->call_arguments().push_back(write_set); @@ -876,7 +876,7 @@ void dfcc_instrumentt::instrument_deallocate_call( INVARIANT(target->is_function_call(), "target must be a function call"); INVARIANT( target->call_function().id() == ID_symbol && - (id2string(to_symbol_expr(target->call_function()).get_identifier()) == + (id2string(to_symbol_expr(target->call_function()).identifier()) == CPROVER_PREFIX "deallocate"), "target must be a call to" CPROVER_PREFIX "deallocate"); @@ -958,7 +958,7 @@ void dfcc_instrumentt::instrument_function_call( const auto &call_function = target->call_function(); if( call_function.id() == ID_symbol && - (id2string(to_symbol_expr(call_function).get_identifier()) == CPROVER_PREFIX + (id2string(to_symbol_expr(call_function).identifier()) == CPROVER_PREFIX "deallocate")) { instrument_deallocate_call(function_id, write_set, target, goto_program); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp index 8626d153409..6e58eaf22a8 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp @@ -48,13 +48,13 @@ void dfcc_is_freeablet::rewrite_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(fun_name == CPROVER_PREFIX "is_freeable") { // redirect call to library implementation to_symbol_expr(target->call_function()) - .set_identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE)); + .identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE)); target->call_arguments().push_back(cfg_info.get_write_set(target)); } else if(fun_name == CPROVER_PREFIX "was_freed") @@ -71,7 +71,7 @@ void dfcc_is_freeablet::rewrite_calls( // redirect call to library implementation to_symbol_expr(target->call_function()) - .set_identifier(library.get_dfcc_fun_name(dfcc_funt::WAS_FREED)); + .identifier(library.get_dfcc_fun_name(dfcc_funt::WAS_FREED)); target->call_arguments().push_back(cfg_info.get_write_set(target)); } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp index 0432df1b9e9..60964cfb398 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp @@ -51,7 +51,7 @@ void dfcc_is_fresht::rewrite_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(has_prefix(id2string(fun_name), CPROVER_PREFIX "is_fresh")) { // add address on first operand @@ -60,7 +60,7 @@ void dfcc_is_fresht::rewrite_calls( // fix the function name. to_symbol_expr(target->call_function()) - .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name); + .identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name); // pass the may_fail flag if(function.source_location().get_bool("no_fail")) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 028893f05d9..e2964050d6c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -485,12 +485,12 @@ void dfcc_libraryt::fix_malloc_free_calls() if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(fun_name == (CONTRACTS_PREFIX "malloc")) - to_symbol_expr(ins->call_function()).set_identifier("malloc"); + to_symbol_expr(ins->call_function()).identifier("malloc"); else if(fun_name == (CONTRACTS_PREFIX "free")) - to_symbol_expr(ins->call_function()).set_identifier("free"); + to_symbol_expr(ins->call_function()).identifier("free"); } } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 52034128cd6..3e4dab5c637 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -65,7 +65,7 @@ bool dfcc_lift_memory_predicatest::calls_memory_predicates( instruction.call_function().id() == ID_symbol) { const auto &callee_id = - to_symbol_expr(instruction.call_function()).get_identifier(); + to_symbol_expr(instruction.call_function()).identifier(); if( is_core_memory_predicate(callee_id) || @@ -154,7 +154,7 @@ std::set dfcc_lift_memory_predicatest::lift_predicates( instruction.call_function().id() == ID_symbol) { const auto &callee = - to_symbol_expr(instruction.call_function()).get_identifier(); + to_symbol_expr(instruction.call_function()).identifier(); if(predicates.find(callee) != predicates.end()) { log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) { @@ -196,7 +196,7 @@ static std::optional is_param_expr( } else if(expr.id() == ID_symbol) { - const irep_idt &ident = to_symbol_expr(expr).get_identifier(); + const irep_idt &ident = to_symbol_expr(expr).identifier(); const auto found = parameter_rank.find(ident); if(found != parameter_rank.end()) { @@ -235,7 +235,7 @@ void dfcc_lift_memory_predicatest::collect_parameters_to_lift( if(it.is_function_call() && it.call_function().id() == ID_symbol) { const irep_idt &callee_id = - to_symbol_expr(it.call_function()).get_identifier(); + to_symbol_expr(it.call_function()).identifier(); if(callee_id == CPROVER_PREFIX "pointer_equals") { auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); @@ -355,7 +355,7 @@ void dfcc_lift_memory_predicatest::lift_parameters_and_update_body( { // add address-of to arguments that are passed in lifted position auto &callee_id = - to_symbol_expr(instruction.call_function()).get_identifier(); + to_symbol_expr(instruction.call_function()).identifier(); if(is_lifted_function(callee_id)) { for(const auto &rank : lifted_parameters[callee_id]) @@ -422,7 +422,7 @@ void dfcc_lift_memory_predicatest::fix_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(is_lifted_function(fun_name)) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp index 44503a0a5fa..7d878485fb9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp @@ -56,7 +56,7 @@ void dfcc_obeys_contractt::get_contract_name( to_address_of_expr(expr).object().id() == ID_symbol, "symbol expression expected"); function_pointer_contracts.insert( - to_symbol_expr(to_address_of_expr(expr).object()).get_identifier()); + to_symbol_expr(to_address_of_expr(expr).object()).identifier()); } } @@ -75,7 +75,7 @@ void dfcc_obeys_contractt::rewrite_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(has_prefix(id2string(fun_name), CPROVER_PREFIX "obeys_contract")) { @@ -85,7 +85,7 @@ void dfcc_obeys_contractt::rewrite_calls( // fix the function name. to_symbol_expr(target->call_function()) - .set_identifier( + .identifier( library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name); // pass the may_fail flag diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp index 5e81637b8cc..1f963e356c0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp @@ -56,7 +56,7 @@ void dfcc_pointer_equalst::rewrite_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(has_prefix(id2string(fun_name), CPROVER_PREFIX "pointer_equals")) { @@ -66,7 +66,7 @@ void dfcc_pointer_equalst::rewrite_calls( // fix the function name. to_symbol_expr(target->call_function()) - .set_identifier( + .identifier( library.dfcc_fun_symbol[dfcc_funt::POINTER_EQUALS].name); // pass the may_fail flag diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp index d0637d393de..172f4355b01 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp @@ -53,7 +53,7 @@ void dfcc_pointer_in_ranget::rewrite_calls( if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(has_prefix( id2string(fun_name), CPROVER_PREFIX "pointer_in_range_dfcc")) @@ -64,7 +64,7 @@ void dfcc_pointer_in_ranget::rewrite_calls( // fix the function name. to_symbol_expr(target->call_function()) - .set_identifier( + .identifier( library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name); // pass the may_fail flag diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp index 6290a235fb4..944f61b9d85 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.cpp @@ -114,7 +114,7 @@ static exprt slice_op_to_deref(const exprt &expr) INVARIANT( function_expr.id() == ID_symbol, "no function pointer calls in loop assigns clause targets"); - auto function_id = to_symbol_expr(function_expr).get_identifier(); + auto function_id = to_symbol_expr(function_expr).identifier(); INVARIANT( function_id == CPROVER_PREFIX "assignable" || function_id == CPROVER_PREFIX "object_whole" || diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 560a148bb3a..48a55bbc323 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -169,7 +169,7 @@ void dfcc_spec_functionst::generate_havoc_instructions( } const irep_idt &callee_id = - to_symbol_expr(ins_it->call_function()).get_identifier(); + to_symbol_expr(ins_it->call_function()).identifier(); // Only process built-in functions that represent assigns clause targets, // and error-out on any other function call @@ -327,7 +327,7 @@ void dfcc_spec_functionst::to_spec_assigns_instructions( } const irep_idt &callee_id = - to_symbol_expr(ins_it->call_function()).get_identifier(); + to_symbol_expr(ins_it->call_function()).identifier(); // Only process built-in functions that specify assignable targets // and error-out on any other function call @@ -407,7 +407,7 @@ void dfcc_spec_functionst::to_spec_frees_instructions( } const irep_idt &callee_id = - to_symbol_expr(ins_it->call_function()).get_identifier(); + to_symbol_expr(ins_it->call_function()).identifier(); // only process the built-in `freeable` function // error out on any other function call diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 9124f954e8d..25bd5ed87ea 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -580,7 +580,7 @@ void disable_may_fail_rec(exprt &expr, bool no_fail) exprt &function = side_effect.operands()[0]; if(function.id() == ID_symbol) { - const irep_idt &func_name = to_symbol_expr(function).get_identifier(); + const irep_idt &func_name = to_symbol_expr(function).identifier(); if(dfcc_is_cprover_pointer_predicate(func_name)) { function.add_source_location().set("no_fail", no_fail); diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index c3b6d2efa1a..b346f64007c 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -152,7 +152,7 @@ void instrument_spec_assignst::check_inclusion_assignment( // Don't check assignable for CPROVER symbol if( lhs.id() == ID_symbol && - has_prefix(id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX)) + has_prefix(id2string(to_symbol_expr(lhs).identifier()), CPROVER_PREFIX)) { return; } @@ -263,7 +263,7 @@ void instrument_spec_assignst::traverse_instructions( PRECONDITION_WITH_DIAGNOSTICS( fun_expr.id() == ID_symbol, "Local static search requires function pointer removal"); - const irep_idt &fun_id = to_symbol_expr(fun_expr).get_identifier(); + const irep_idt &fun_id = to_symbol_expr(fun_expr).identifier(); const auto &found = functions.function_map.find(fun_id); INVARIANT( @@ -391,7 +391,7 @@ void instrument_spec_assignst::instrument_instructions( // are not automatically tracked in the stack_allocated map, // so to be writable these variables must be listed in the assigns // clause. - log.warning() << "Found a `DEAD` variable " << symbol.get_identifier() + log.warning() << "Found a `DEAD` variable " << symbol.identifier() << " without corresponding `DECL`, at: " << instruction_it->source_location() << messaget::eom; } @@ -507,7 +507,7 @@ car_exprt instrument_spec_assignst::create_car_expr( const auto &funcall = to_side_effect_expr_function_call(target); if(can_cast_expr(funcall.function())) { - const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + const auto &ident = to_symbol_expr(funcall.function()).identifier(); PRECONDITION_WITH_DIAGNOSTICS( ident == CPROVER_PREFIX "object_from" || @@ -940,7 +940,7 @@ bool instrument_spec_assignst::must_check_assign( { const auto &symbol_expr = to_symbol_expr(target->assign_lhs()); - if(cfg_info.is_local(symbol_expr.get_identifier())) + if(cfg_info.is_local(symbol_expr.identifier())) { log.debug() << LOG_HEADER << "skipping checking on assignment to local symbol " @@ -1003,7 +1003,7 @@ bool instrument_spec_assignst::must_track_decl( const goto_programt::const_targett &target) const { log.debug().source_location = target->source_location(); - if(must_track_decl_or_dead(target->decl_symbol().get_identifier())) + if(must_track_decl_or_dead(target->decl_symbol().identifier())) { log.debug() << LOG_HEADER << "explicitly tracking " << format(target->decl_symbol()) << " as assignable" @@ -1024,7 +1024,7 @@ bool instrument_spec_assignst::must_track_decl( bool instrument_spec_assignst::must_track_dead( const goto_programt::const_targett &target) const { - return must_track_decl_or_dead(target->dead_symbol().get_identifier()); + return must_track_decl_or_dead(target->dead_symbol().identifier()); } void instrument_spec_assignst::instrument_assign_statement( @@ -1048,7 +1048,7 @@ void instrument_spec_assignst::instrument_call_statement( "a function call"); const auto &callee_name = - to_symbol_expr(instruction_it->call_function()).get_identifier(); + to_symbol_expr(instruction_it->call_function()).identifier(); if(callee_name == "malloc") { diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index c0d2dbe5ce6..c78eb140966 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -51,7 +51,7 @@ void functions_in_scope_visitort::operator()(const goto_programt &prog) } else { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(function_set.find(fun_name) == function_set.end()) { function_set.insert(fun_name); @@ -99,7 +99,7 @@ void find_is_fresh_calls_visitort::operator()(goto_programt &prog) if(function.id() == ID_symbol) { - const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + const irep_idt &fun_name = to_symbol_expr(function).identifier(); if(fun_name == (CPROVER_PREFIX + std::string("is_fresh"))) { @@ -230,7 +230,7 @@ void is_fresh_baset::update_fn_call( } // fixing the function name. - to_symbol_expr(ins->call_function()).set_identifier(fn_name); + to_symbol_expr(ins->call_function()).identifier(fn_name); // pass the memory mmap ins->call_arguments().push_back(address_of_exprt( diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index ecd6e779b72..f01bd73f97e 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -121,7 +121,7 @@ void havoc_assigns_targetst::append_havoc_code_for_expr( { const auto &funcall = to_side_effect_expr_function_call(expr); // type-checking ensures the function expression is necessarily a symbol - const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + const auto &ident = to_symbol_expr(funcall.function()).identifier(); if(ident == CPROVER_PREFIX "object_whole") { append_object_havoc_code_for_expr( @@ -351,7 +351,7 @@ void infer_loop_assigns( if(e.id() == ID_symbol) { const auto &s = expr_try_dynamic_cast(e); - return !has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX); + return !has_prefix(id2string(s->identifier()), CPROVER_PREFIX); } return true; }); @@ -536,7 +536,7 @@ bool is_assignment_to_instrumented_variable( if(can_cast_expr(target->assign_lhs())) { const auto &lhs = to_symbol_expr(target->assign_lhs()); - return id2string(lhs.get_identifier()).find("::" + var_name) != + return id2string(lhs.identifier()).find("::" + var_name) != std::string::npos; } diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index bdafcfa5608..d76f7073d56 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -180,7 +180,7 @@ void print_global_state_size(const goto_modelt &goto_model) if(ode.root_object().id() == ID_symbol) { const symbol_exprt &symbol_expr = to_symbol_expr(ode.root_object()); - initialized.insert(symbol_expr.get_identifier()); + initialized.insert(symbol_expr.identifier()); } } } diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index c86e3af073d..5ab081c9490 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -61,7 +61,7 @@ void cover_cover_instrumentert::instrument( const auto &function = i_it->call_function(); if( function.id() == ID_symbol && - to_symbol_expr(function).get_identifier() == CPROVER_PREFIX "cover" && + to_symbol_expr(function).identifier() == CPROVER_PREFIX "cover" && i_it->call_arguments().size() == 1) { const exprt c = i_it->call_arguments()[0]; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index f74233caea8..89e785ca3f3 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -1084,9 +1084,9 @@ void dump_ct::cleanup_harness(code_blockt &b) if(func.id()==ID_symbol) { symbol_exprt &s=to_symbol_expr(func); - if(s.get_identifier()==ID_main) - s.set_identifier(CPROVER_PREFIX+id2string(ID_main)); - else if(s.get_identifier() == INITIALIZE_FUNCTION) + if(s.identifier() == ID_main) + s.identifier(CPROVER_PREFIX + id2string(ID_main)); + else if(s.identifier() == INITIALIZE_FUNCTION) continue; } } @@ -1435,9 +1435,9 @@ void dump_ct::cleanup_expr(exprt &expr) // don't edit function calls we might have introduced const symbolt *s; - if(!ns.lookup(fn.get_identifier(), s)) + if(!ns.lookup(fn.identifier(), s)) { - const symbolt &fn_sym=ns.lookup(fn.get_identifier()); + const symbolt &fn_sym = ns.lookup(fn.identifier()); const code_typet &code_type=to_code_type(fn_sym.type); const code_typet::parameterst ¶meters=code_type.parameters(); diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 1e2b29f125d..736864cdc9d 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -248,7 +248,7 @@ static bool implicit(goto_programt::const_targett target) const symbol_exprt &s = to_symbol_expr(a_lhs); - return s.get_identifier() == rounding_mode_identifier(); + return s.identifier() == rounding_mode_identifier(); } void full_slicert::operator()( @@ -287,12 +287,12 @@ void full_slicert::operator()( else if(instruction->is_decl()) { const auto &s = instruction->decl_symbol(); - decl_dead[s.get_identifier()].push(instruction_node_index); + decl_dead[s.identifier()].push(instruction_node_index); } else if(instruction->is_dead()) { const auto &s = instruction->dead_symbol(); - decl_dead[s.get_identifier()].push(instruction_node_index); + decl_dead[s.identifier()].push(instruction_node_index); } } diff --git a/src/goto-instrument/function_assigns.cpp b/src/goto-instrument/function_assigns.cpp index 06d2e8879d9..f78e8c271ee 100644 --- a/src/goto-instrument/function_assigns.cpp +++ b/src/goto-instrument/function_assigns.cpp @@ -46,7 +46,7 @@ void function_assignst::get_assigns_function( { if(function.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); function_mapt::const_iterator fm_it = function_map.find(identifier); diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 8212478f2a3..dc4c27de008 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -617,7 +617,7 @@ void generate_function_bodies( if(expr.id() != ID_symbol) return false; std::string called_function_name = - id2string(to_symbol_expr(expr).get_identifier()); + id2string(to_symbol_expr(expr).identifier()); if(called_function_name == function_name) return true; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 87eee70ed89..e5978ae1d5a 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -95,7 +95,7 @@ void goto_program2codet::build_dead_map() { if(instruction.is_dead()) { - dead_map[instruction.dead_symbol().get_identifier()] = + dead_map[instruction.dead_symbol().identifier()] = instruction.location_number; } } @@ -460,7 +460,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( CHECK_RETURN(next != goto_program.instructions.end()); // see if decl can go in current dest block - dead_mapt::const_iterator entry=dead_map.find(symbol.get_identifier()); + dead_mapt::const_iterator entry = dead_map.find(symbol.identifier()); bool move_to_dest= &toplevel_block==&dest || (entry!=dead_map.end() && upper_bound->location_number > entry->second); @@ -1525,9 +1525,9 @@ void goto_program2codet::cleanup_function_call( // don't edit function calls we might have introduced const symbolt *s; - if(!ns.lookup(fn.get_identifier(), s)) + if(!ns.lookup(fn.identifier(), s)) { - const symbolt &fn_sym=ns.lookup(fn.get_identifier()); + const symbolt &fn_sym = ns.lookup(fn.identifier()); const code_typet &code_type=to_code_type(fn_sym.type); const code_typet::parameterst ¶meters=code_type.parameters(); @@ -1957,7 +1957,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) { if(expr.type().id()!=ID_code) { - const irep_idt &identifier=to_symbol_expr(expr).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr).identifier(); const symbolt &symbol=ns.lookup(identifier); if(symbol.is_static_lifetime && diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp index d0202e60d64..5f29f9dedfb 100644 --- a/src/goto-instrument/horn_encoding.cpp +++ b/src/goto-instrument/horn_encoding.cpp @@ -712,7 +712,7 @@ void state_encodingt::function_call_symbol( { const auto &function = to_symbol_expr(loc->call_function()); const auto &type = to_code_type(function.type()); - auto identifier = function.get_identifier(); + auto identifier = function.identifier(); auto new_annotation = annotation + u8" \u2192 " + id2string(identifier); dest.annotation(new_annotation); @@ -896,8 +896,8 @@ void state_encodingt::encode( else if( lhs.id() == ID_symbol && has_prefix( - id2string(to_symbol_expr(lhs).get_identifier()), CPROVER_PREFIX) && - to_symbol_expr(lhs).get_identifier() != CPROVER_PREFIX "rounding_mode") + id2string(to_symbol_expr(lhs).identifier()), CPROVER_PREFIX) && + to_symbol_expr(lhs).identifier() != CPROVER_PREFIX "rounding_mode") { // skip for now dest << equal_exprt(out_state_expr(loc), in_state_expr(loc)); @@ -1142,9 +1142,8 @@ void variable_encoding(std::vector &constraints) std::sort( variables.begin(), variables.end(), - [](const symbol_exprt &a, const symbol_exprt &b) { - return id2string(a.get_identifier()) < id2string(b.get_identifier()); - }); + [](const symbol_exprt &a, const symbol_exprt &b) + { return id2string(a.identifier()) < id2string(b.identifier()); }); for(auto &c : constraints) c = variable_encoding(c, variables); @@ -1173,7 +1172,7 @@ void equality_propagation(std::vector &constraints) const auto &symbol_expr = to_symbol_expr(equal_expr.lhs()); // this is a (deliberate) no-op when the symbol is already in the map - if(values.replaces_symbol(symbol_expr.get_identifier())) + if(values.replaces_symbol(symbol_expr.identifier())) { } else diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index 4f082d05ac7..cfc83340aec 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -205,7 +205,7 @@ void interrupt( if( gf_entry.first != INITIALIZE_FUNCTION && gf_entry.first != goto_functionst::entry_point() && - gf_entry.first != isr.get_identifier()) + gf_entry.first != isr.identifier()) { interrupt( value_sets, diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 2306737d06b..e49b20a0255 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -177,8 +177,9 @@ bool model_argc_argv( if(main_call->is_function_call()) { const exprt &func = main_call->call_function(); - if(func.id()==ID_symbol && - to_symbol_expr(func).get_identifier()==main_symbol.name) + if( + func.id() == ID_symbol && + to_symbol_expr(func).identifier() == main_symbol.name) break; } } diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 7c7e7170ec8..56266f83372 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -37,7 +37,7 @@ bool is_nondet_initializable_static( const symbol_exprt &symbol_expr, const namespacet &ns) { - const irep_idt &id = symbol_expr.get_identifier(); + const irep_idt &id = symbol_expr.identifier(); // is it a __CPROVER_* variable? if(id.starts_with(CPROVER_PREFIX)) @@ -103,7 +103,7 @@ static void nondet_static( side_effect_expr_nondett nondet{ sym.type(), instruction.source_location()}; instruction.assign_rhs_nonconst() = nondet; - goto_model.symbol_table.get_writeable_ref(sym.get_identifier()).value = + goto_model.symbol_table.get_writeable_ref(sym.identifier()).value = nondet; } } @@ -112,9 +112,9 @@ static void nondet_static( const symbol_exprt &fsym = to_symbol_expr(instruction.call_function()); // see cpp/cpp_typecheck.cpp, which creates initialization functions - if(fsym.get_identifier().starts_with("#cpp_dynamic_initialization#")) + if(fsym.identifier().starts_with("#cpp_dynamic_initialization#")) { - nondet_static(ns, goto_model, fsym.get_identifier()); + nondet_static(ns, goto_model, fsym.identifier()); } } } diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index a145c106496..a8146df8806 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -115,7 +115,7 @@ void nondet_volatilet::handle_volatile_expression( if( all_nondet || (expr.id() == ID_symbol && - nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0)) + nondet_variables.count(to_symbol_expr(expr).identifier()) != 0)) { typet t = expr.type(); t.remove(ID_C_volatile); @@ -133,7 +133,7 @@ void nondet_volatilet::handle_volatile_expression( return; } - const irep_idt &id = to_symbol_expr(expr).get_identifier(); + const irep_idt &id = to_symbol_expr(expr).identifier(); const auto &it = variable_models.find(id); if(it == variable_models.end()) diff --git a/src/goto-instrument/object_id.h b/src/goto-instrument/object_id.h index acdcbdd625e..c6fee15c37f 100644 --- a/src/goto-instrument/object_id.h +++ b/src/goto-instrument/object_id.h @@ -26,7 +26,7 @@ class object_idt explicit object_idt(const symbol_exprt &symbol_expr) { - id=symbol_expr.get_identifier(); + id = symbol_expr.identifier(); } explicit object_idt(const irep_idt &identifier) diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index fce1b27d0ed..6a4c48e493f 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -120,7 +120,7 @@ static std::string comment(const rw_set_baset::entryt &entry, bool write) static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) { - const irep_idt &identifier=symbol_expr.get_identifier(); + const irep_idt &identifier = symbol_expr.identifier(); if( identifier == CPROVER_PREFIX "alloc" || diff --git a/src/goto-instrument/replace_calls.cpp b/src/goto-instrument/replace_calls.cpp index bf7d64e8772..06812af2328 100644 --- a/src/goto-instrument/replace_calls.cpp +++ b/src/goto-instrument/replace_calls.cpp @@ -74,7 +74,7 @@ void replace_callst::operator()( PRECONDITION(function.id() == ID_symbol); const symbol_exprt &se = to_symbol_expr(function); - const irep_idt &id = se.get_identifier(); + const irep_idt &id = se.identifier(); auto f_it1 = goto_functions.function_map.find(id); @@ -108,7 +108,7 @@ void replace_callst::operator()( // Finally modify the call ins.call_function().type() = ns.lookup(f_it2->first).type; - to_symbol_expr(ins.call_function()).set_identifier(new_id); + to_symbol_expr(ins.call_function()).identifier(new_id); } } diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index b1c03a6c273..14850b3333c 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -87,7 +87,7 @@ void _rw_set_loct::read_write_rec( { const symbol_exprt &symbol_expr=to_symbol_expr(expr); - irep_idt object=id2string(symbol_expr.get_identifier())+suffix; + irep_idt object = id2string(symbol_expr.identifier()) + suffix; if(r) { @@ -194,7 +194,7 @@ void rw_set_functiont::compute_rec(const exprt &function) { if(function.id()==ID_symbol) { - const irep_idt &function_id = to_symbol_expr(function).get_identifier(); + const irep_idt &function_id = to_symbol_expr(function).identifier(); goto_functionst::function_mapt::const_iterator f_it = goto_functions.function_map.find(function_id); diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 5590f370fcf..9635dd2546e 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -66,7 +66,7 @@ void thread_exit_instrumentation(goto_modelt &goto_model) { const exprt &function = instruction.call_function(); if(function.id()==ID_symbol) - thread_fkts.insert(to_symbol_expr(function).get_identifier()); + thread_fkts.insert(to_symbol_expr(function).identifier()); } } } diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-instrument/undefined_functions.cpp index 6a71afeebfe..4118b18d7aa 100644 --- a/src/goto-instrument/undefined_functions.cpp +++ b/src/goto-instrument/undefined_functions.cpp @@ -47,7 +47,7 @@ void undefined_function_abort_path(goto_modelt &goto_model) continue; const irep_idt &function_identifier = - to_symbol_expr(function).get_identifier(); + to_symbol_expr(function).identifier(); goto_functionst::function_mapt::const_iterator entry = goto_model.goto_functions.function_map.find(function_identifier); diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index a4b1cc1b58b..93c1e13d879 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -48,7 +48,7 @@ void uninitializedt::get_tracking(goto_programt::const_targett i_it) { if(object.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(object).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).identifier(); const std::set &uninitialized= uninitialized_analysis[i_it].uninitialized; if(uninitialized.find(identifier)!=uninitialized.end()) @@ -101,7 +101,7 @@ void uninitializedt::add_assertions( // if we track it, add declaration and assignment // for tracking variable! - const irep_idt &identifier = instruction.decl_symbol().get_identifier(); + const irep_idt &identifier = instruction.decl_symbol().identifier(); if(tracking.find(identifier)!=tracking.end()) { @@ -138,7 +138,7 @@ void uninitializedt::add_assertions( { if(object.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(object).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).identifier(); if(uninitialized.find(identifier)!=uninitialized.end()) { @@ -166,7 +166,7 @@ void uninitializedt::add_assertions( { if(object.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(object).get_identifier(); + const irep_idt &identifier = to_symbol_expr(object).identifier(); if(tracking.find(identifier)!=tracking.end()) { diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp index 0ba50d26470..2a7e7bebd7e 100644 --- a/src/goto-instrument/value_set_fi_fp_removal.cpp +++ b/src/goto-instrument/value_set_fi_fp_removal.cpp @@ -65,7 +65,7 @@ void value_set_fi_fp_removal( for(const auto &f : functions) message.status() - << " function: " << f.get_identifier() << messaget::eom; + << " function: " << f.identifier() << messaget::eom; if(functions.size() > 0) { diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index fc33f29f75b..94955668ee0 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -694,7 +694,7 @@ void instrumentert::cfg_visitort::visit_cfg_function_call( const goto_programt::instructiont &instruction=*i_it; const exprt &fun = instruction.call_function(); - const irep_idt &fun_id=to_symbol_expr(fun).get_identifier(); + const irep_idt &fun_id = to_symbol_expr(fun).identifier(); /* ignore recursive calls -- underapproximation */ try { diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index b4140f288fd..55adf6f536c 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -937,7 +937,7 @@ bool shared_bufferst::is_buffered( // the source_location in the code (true) ) { - const irep_idt &identifier=symbol_expr.get_identifier(); + const irep_idt &identifier = symbol_expr.identifier(); if( identifier == CPROVER_PREFIX "alloc" || @@ -971,7 +971,7 @@ bool shared_bufferst::is_buffered_in_general( if(cav11) return true; - const irep_idt &identifier=symbol_expr.get_identifier(); + const irep_idt &identifier = symbol_expr.identifier(); const source_locationt &source_location=symbol_expr.source_location(); if(cycles.find(identifier)==cycles.end()) @@ -1322,7 +1322,7 @@ void shared_bufferst::cfg_visitort::weak_memory( else if(instruction.is_function_call()) { const exprt &fun = instruction.call_function(); - weak_memory(value_sets, to_symbol_expr(fun).get_identifier(), model); + weak_memory(value_sets, to_symbol_expr(fun).identifier(), model); } } } diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index 22e6c44abd8..5c0b1ca9fa5 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -396,8 +396,7 @@ void cfg_baset::compute_edges_function_call( if(function.id()!=ID_symbol) return; - const irep_idt &identifier= - to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); goto_functionst::function_mapt::const_iterator f_it= goto_functions.function_map.find(identifier); diff --git a/src/goto-programs/compute_called_functions.cpp b/src/goto-programs/compute_called_functions.cpp index 50e4a90bcbf..1e66066d1a0 100644 --- a/src/goto-programs/compute_called_functions.cpp +++ b/src/goto-programs/compute_called_functions.cpp @@ -34,7 +34,7 @@ void compute_address_taken_functions( { const exprt &target = address.object(); if(target.id() == ID_symbol) - address_taken.insert(to_symbol_expr(target).get_identifier()); + address_taken.insert(to_symbol_expr(target).identifier()); } } } @@ -49,7 +49,7 @@ void compute_functions( if(src.type().id()==ID_code && src.id()==ID_symbol) - address_taken.insert(to_symbol_expr(src).get_identifier()); + address_taken.insert(to_symbol_expr(src).identifier()); } /// get all functions whose address is taken diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 7ecdaa7a6fc..61e85ca0264 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -199,7 +199,7 @@ void goto_partial_inline( continue; const symbol_exprt &symbol_expr=to_symbol_expr(function_expr); - const irep_idt id=symbol_expr.get_identifier(); + const irep_idt id = symbol_expr.identifier(); goto_functionst::function_mapt::const_iterator called_it = goto_functions.function_map.find(id); diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 15ffd84048e..c604403bb8d 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -223,7 +223,7 @@ void goto_inlinet::insert_function_body( PRECONDITION(!dest.empty()); PRECONDITION(goto_function.body_available()); - const irep_idt identifier=function.get_identifier(); + const irep_idt identifier = function.identifier(); goto_programt body; body.copy_from(goto_function.body); @@ -326,7 +326,7 @@ void goto_inlinet::expand_function_call( const symbol_exprt &function=to_symbol_expr(function_expr); - const irep_idt identifier=function.get_identifier(); + const irep_idt identifier = function.identifier(); if(is_ignored(identifier)) return; diff --git a/src/goto-programs/goto_instruction_code.h b/src/goto-programs/goto_instruction_code.h index 946cbe61119..298893c01eb 100644 --- a/src/goto-programs/goto_instruction_code.h +++ b/src/goto-programs/goto_instruction_code.h @@ -147,7 +147,7 @@ class code_deadt : public goto_instruction_codet const irep_idt &get_identifier() const { - return symbol().get_identifier(); + return symbol().identifier(); } static void check( @@ -220,7 +220,7 @@ class code_declt : public goto_instruction_codet const irep_idt &get_identifier() const { - return symbol().get_identifier(); + return symbol().identifier(); } static void check( @@ -233,7 +233,7 @@ class code_declt : public goto_instruction_codet vm, code.op0().id() == ID_symbol, "declaring a non-symbol: " + - id2string(to_symbol_expr(code.op0()).get_identifier())); + id2string(to_symbol_expr(code.op0()).identifier())); } }; diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 2539394b69a..360759e4a1e 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -329,7 +329,7 @@ void goto_programt::get_decl_identifiers( DATA_INVARIANT( instruction.code().operands().size() == 1, "declaration statement expects one operand"); - decl_identifiers.insert(instruction.decl_symbol().get_identifier()); + decl_identifiers.insert(instruction.decl_symbol().identifier()); } } } @@ -808,7 +808,7 @@ void goto_programt::instructiont::validate( if(e.id() == ID_symbol) { const auto &goto_symbol_expr = to_symbol_expr(e); - const auto &goto_id = goto_symbol_expr.get_identifier(); + const auto &goto_id = goto_symbol_expr.identifier(); const symbolt *table_symbol; if(!ns.lookup(goto_id, table_symbol)) @@ -944,9 +944,9 @@ void goto_programt::instructiont::validate( source_location()); DATA_CHECK_WITH_DIAGNOSTICS( vm, - !ns.lookup(decl_symbol().get_identifier(), table_symbol), + !ns.lookup(decl_symbol().identifier(), table_symbol), "declared symbols should be known", - id2string(decl_symbol().get_identifier()), + id2string(decl_symbol().identifier()), source_location()); break; case DEAD: @@ -957,9 +957,9 @@ void goto_programt::instructiont::validate( source_location()); DATA_CHECK_WITH_DIAGNOSTICS( vm, - !ns.lookup(dead_symbol().get_identifier(), table_symbol), + !ns.lookup(dead_symbol().identifier(), table_symbol), "removed symbols should be known", - id2string(dead_symbol().get_identifier()), + id2string(dead_symbol().identifier()), source_location()); break; case FUNCTION_CALL: diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index c3e283978fa..4cc086e827e 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -297,7 +297,7 @@ static void trace_value( irep_idt identifier; if(lhs_object.has_value()) - identifier=lhs_object->get_identifier(); + identifier = lhs_object->identifier(); out << from_expr(ns, identifier, full_lhs) << '='; diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 239922a2ab3..cf6c154bb4b 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -47,14 +47,13 @@ void graphml_witnesst::remove_l0_l1(exprt &expr) expr=to_ssa_expr(expr).get_original_expr(); else { - std::string identifier= - id2string(to_symbol_expr(expr).get_identifier()); + std::string identifier = id2string(to_symbol_expr(expr).identifier()); std::string::size_type l0_l1=identifier.find_first_of("!@"); if(l0_l1!=std::string::npos) { identifier.resize(l0_l1); - to_symbol_expr(expr).set_identifier(identifier); + to_symbol_expr(expr).identifier(identifier); } } @@ -261,7 +260,7 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) { if( expr.id() == ID_symbol && - to_symbol_expr(expr).get_identifier().starts_with(prefix)) + to_symbol_expr(expr).identifier().starts_with(prefix)) { return true; } @@ -439,7 +438,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) it->type == goto_trace_stept::typet::ASSIGNMENT && lhs_object.has_value()) { - const std::string &lhs_id = id2string(lhs_object->get_identifier()); + const std::string &lhs_id = id2string(lhs_object->identifier()); if(lhs_id.find("pthread_create::thread") != std::string::npos) { xmlt &data_t = edge.new_element("data"); diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index 0f1fd3cbd7a..534f0a9e430 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -19,7 +19,7 @@ std::vector get_preconditions( const symbol_exprt &function, const goto_functionst &goto_functions) { - const irep_idt &identifier=function.get_identifier(); + const irep_idt &identifier = function.identifier(); auto f_it=goto_functions.function_map.find(identifier); if(f_it==goto_functions.function_map.end()) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 8ad54ddbf2d..83ad4802f6c 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -703,8 +703,8 @@ void interpretert::assign( if(show) { output.status() << total_steps << " ** assigning " - << address_to_symbol(address_val).get_identifier() - << "[" << address_to_offset(address_val) + << address_to_symbol(address_val).identifier() << "[" + << address_to_offset(address_val) << "]:=" << rhs[numeric_cast_v(i)] << "\n" << messaget::eom; } @@ -751,7 +751,7 @@ void interpretert::execute_function_call() #if 0 const memory_cellt &cell=memory[address]; #endif - const irep_idt identifier = address_to_symbol(address).get_identifier(); + const irep_idt identifier = address_to_symbol(address).identifier(); trace_step.called_function = identifier; const goto_functionst::function_mapt::const_iterator f_it= @@ -817,7 +817,7 @@ void interpretert::execute_function_call() else { list_input_varst::iterator it = - function_input_vars.find(to_symbol_expr(call_function).get_identifier()); + function_input_vars.find(to_symbol_expr(call_function).identifier()); if(it!=function_input_vars.end()) { @@ -910,15 +910,15 @@ mp_integer interpretert::build_memory_map(const symbol_exprt &symbol_expr) { typet alloc_type = concretize_type(symbol_expr.type()); mp_integer size=get_size(alloc_type); - auto it = dynamic_types.find(symbol_expr.get_identifier()); + auto it = dynamic_types.find(symbol_expr.identifier()); if(it!=dynamic_types.end()) { - mp_integer address = memory_map[symbol_expr.get_identifier()]; + mp_integer address = memory_map[symbol_expr.identifier()]; mp_integer current_size=base_address_to_alloc_size(address); // current size <= size already recorded if(size<=current_size) - return memory_map[symbol_expr.get_identifier()]; + return memory_map[symbol_expr.identifier()]; } // The current size is bigger then the one previously recorded @@ -929,10 +929,10 @@ mp_integer interpretert::build_memory_map(const symbol_exprt &symbol_expr) mp_integer address=memory.size(); memory.resize(numeric_cast_v(address + size)); - memory_map[symbol_expr.get_identifier()] = address; + memory_map[symbol_expr.identifier()] = address; inverse_memory_map[address] = symbol_expr; dynamic_types.insert( - std::pair(symbol_expr.get_identifier(), alloc_type)); + std::pair(symbol_expr.identifier(), alloc_type)); return address; } @@ -1048,7 +1048,7 @@ void interpretert::print_memory(bool input_flags) { mp_integer i=cell_address.first; const memory_cellt &cell=cell_address.second; - const auto identifier = address_to_symbol(i).get_identifier(); + const auto identifier = address_to_symbol(i).identifier(); const auto offset=address_to_offset(i); output.status() << identifier << "[" << offset << "]" << "=" << cell.value << messaget::eom; diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 3590fe63190..4b65039e10f 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -1000,7 +1000,7 @@ mp_integer interpretert::evaluate_address( { const irep_idt &identifier = is_ssa_expr(expr) ? to_ssa_expr(expr).get_original_name() - : to_symbol_expr(expr).get_identifier(); + : to_symbol_expr(expr).identifier(); interpretert::memory_mapt::const_iterator m_it1= memory_map.find(identifier); diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp index b7f13081e39..3af77d5e51a 100644 --- a/src/goto-programs/json_expr.cpp +++ b/src/goto-programs/json_expr.cpp @@ -327,7 +327,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode) CHECK_RETURN(!error); result["type"] = json_stringt(type_string); - const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier(); + const irep_idt &ptr_id = to_symbol_expr(simpl_expr).identifier(); identifiert identifier(id2string(ptr_id)); DATA_INVARIANT( !identifier.components.empty(), diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index d8eb7649637..94ef5d74d00 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -69,7 +69,7 @@ void convert_decl( auto lhs_object=step.get_lhs_object(); irep_idt identifier = - lhs_object.has_value()?lhs_object->get_identifier():irep_idt(); + lhs_object.has_value() ? lhs_object->identifier() : irep_idt(); json_assignment["stepType"] = json_stringt("assignment"); diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index d4c684d1ddf..e17619bb882 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -182,9 +182,9 @@ void finalize_linking( const symbolt &symbol = symbol_pair.second; INVARIANT(symbol.value.id() == ID_symbol, "must have symbol"); - const irep_idt &id = to_symbol_expr(symbol.value).get_identifier(); + const irep_idt &id = to_symbol_expr(symbol.value).identifier(); - #if 0 +#if 0 if(!base_type_eq(symbol.type, ns.lookup(id).type, ns)) { std::cerr << symbol << '\n'; @@ -192,7 +192,7 @@ void finalize_linking( } INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns), "type matches"); - #endif +#endif macro_application.insert_expr(symbol.name, id); } diff --git a/src/goto-programs/parameter_assignments.cpp b/src/goto-programs/parameter_assignments.cpp index 9bea3c04f3b..b58565ff2c4 100644 --- a/src/goto-programs/parameter_assignments.cpp +++ b/src/goto-programs/parameter_assignments.cpp @@ -47,7 +47,7 @@ void parameter_assignmentst::do_function_calls( PRECONDITION(as_const(*i_it).call_function().id() == ID_symbol); const irep_idt &identifier = - to_symbol_expr(as_const(*i_it).call_function()).get_identifier(); + to_symbol_expr(as_const(*i_it).call_function()).identifier(); // see if we have it const namespacet ns(symbol_table); diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp index 3384430a310..8f5caaba0ba 100644 --- a/src/goto-programs/remove_calls_no_body.cpp +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -76,7 +76,7 @@ bool remove_calls_no_bodyt::is_opaque_function_call( return false; const symbol_exprt &se = to_symbol_expr(f); - const irep_idt id = se.get_identifier(); + const irep_idt id = se.identifier(); goto_functionst::function_mapt::const_iterator f_it = goto_functions.function_map.find(id); @@ -108,7 +108,7 @@ void remove_calls_no_bodyt::operator()( { messaget log{message_handler}; log.status() << "Removing call to " - << to_symbol_expr(it->call_function()).get_identifier() + << to_symbol_expr(it->call_function()).identifier() << ", which has no body" << messaget::eom; remove_call_no_body( goto_program, it, it->call_lhs(), it->call_arguments()); diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index 349855e122c..f335cc7230f 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -73,7 +73,7 @@ exprt remove_const_function_pointerst::replace_const_symbols( if(is_const_expression(expression)) { const symbolt &symbol = - symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier()); + symbol_table.lookup_ref(to_symbol_expr(expression).identifier()); if(symbol.type.id() != ID_code && symbol.value.is_not_nil()) { const exprt &symbol_value=symbol.value; @@ -109,7 +109,7 @@ exprt remove_const_function_pointerst::replace_const_symbols( exprt remove_const_function_pointerst::resolve_symbol( const symbol_exprt &symbol_expr) const { - const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.get_identifier()); + const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.identifier()); return symbol.value; } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 1be6140690e..f29132d96b7 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -221,7 +221,7 @@ static void fix_return_type( const namespacet ns(symbol_table); const symbolt &function_symbol = - ns.lookup(to_symbol_expr(function_call.function()).get_identifier()); + ns.lookup(to_symbol_expr(function_call.function()).identifier()); symbolt &tmp_symbol = get_fresh_aux_symbol( code_type.return_type(), @@ -353,7 +353,7 @@ static std::string function_pointer_assertion_comment( if(candidates.size() == 1) { - comment << candidates.begin()->get_identifier(); + comment << candidates.begin()->identifier(); } else if(candidates.empty()) { @@ -368,7 +368,7 @@ static std::string function_pointer_assertion_comment( candidates.begin(), candidates.end(), ", ", - [](const symbol_exprt &s) { return s.get_identifier(); }); + [](const symbol_exprt &s) { return s.identifier(); }); comment << ']'; } @@ -474,7 +474,7 @@ void remove_function_pointer( if(!first) mstream << ", "; - mstream << function.get_identifier(); + mstream << function.identifier(); first = false; } diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 56381490a53..4c80d68167d 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -68,7 +68,7 @@ remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id) { const namespacet ns(symbol_table); const auto symbol_expr = return_value_symbol(function_id, ns); - const auto symbol_name = symbol_expr.get_identifier(); + const auto symbol_name = symbol_expr.identifier(); if(symbol_table.has_symbol(symbol_name)) return symbol_expr; @@ -162,7 +162,7 @@ bool remove_returnst::do_function_calls( "remove-returns"); const irep_idt function_id = - to_symbol_expr(i_it->call_function()).get_identifier(); + to_symbol_expr(i_it->call_function()).identifier(); // Do we return anything? if(does_function_call_return(*i_it)) @@ -314,7 +314,7 @@ bool remove_returnst::restore_returns( { if( instruction.assign_lhs().id() != ID_symbol || - to_symbol_expr(instruction.assign_lhs()).get_identifier() != rv_name_id) + to_symbol_expr(instruction.assign_lhs()).identifier() != rv_name_id) { continue; } @@ -348,7 +348,7 @@ void remove_returnst::undo_function_calls( continue; const irep_idt function_id = - to_symbol_expr(i_it->call_function()).get_identifier(); + to_symbol_expr(i_it->call_function()).identifier(); // find "f(...); lhs=f#return_value; DEAD f#return_value;" // and revert to "lhs=f(...);" @@ -424,7 +424,7 @@ bool is_return_value_identifier(const irep_idt &id) bool is_return_value_symbol(const symbol_exprt &symbol_expr) { - return is_return_value_identifier(symbol_expr.get_identifier()); + return is_return_value_identifier(symbol_expr.identifier()); } bool does_function_call_return(const goto_programt::instructiont &function_call) diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp index 17a8cec60db..d4f0fbdada3 100644 --- a/src/goto-programs/remove_unused_functions.cpp +++ b/src/goto-programs/remove_unused_functions.cpp @@ -77,8 +77,7 @@ void find_used_functions( { const auto &function = instruction.call_function(); - const irep_idt &identifier = - to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); find_used_functions(identifier, functions, seen); } diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 21d96041a1e..e3d9822813c 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -103,7 +103,7 @@ static void create_static_function_call( // type (in Java, for example, we see ArrayList.add(ArrayList::E arg) // overriding Collection.add(Collection::E arg)) const auto &callee_parameters = - to_code_type(ns.lookup(function_symbol.get_identifier()).type).parameters(); + to_code_type(ns.lookup(function_symbol.identifier()).type).parameters(); auto &call_args = call.arguments(); INVARIANT( @@ -360,9 +360,8 @@ static goto_programt::targett replace_virtual_function_with_dispatch_table( for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it) { const auto &fun=*it; - irep_idt id_or_empty = fun.symbol_expr.has_value() - ? fun.symbol_expr->get_identifier() - : irep_idt(); + irep_idt id_or_empty = + fun.symbol_expr.has_value() ? fun.symbol_expr->identifier() : irep_idt(); auto insertit = calls.insert({id_or_empty, goto_programt::targett()}); // Only create one call sequence per possible target: @@ -523,7 +522,7 @@ void get_virtual_calleest::get_child_functions_rec( if( it != entry_map.end() && (!it->second.symbol_expr.has_value() || - !it->second.symbol_expr->get_identifier().starts_with( + !it->second.symbol_expr->identifier().starts_with( "java::java.lang.Object"))) { continue; @@ -610,13 +609,12 @@ void get_virtual_calleest::get_functions( std::sort( functions.begin(), functions.end(), - [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) { - irep_idt a_id = a.symbol_expr.has_value() - ? a.symbol_expr->get_identifier() - : irep_idt(); - irep_idt b_id = b.symbol_expr.has_value() - ? b.symbol_expr->get_identifier() - : irep_idt(); + [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) + { + irep_idt a_id = + a.symbol_expr.has_value() ? a.symbol_expr->identifier() : irep_idt(); + irep_idt b_id = + b.symbol_expr.has_value() ? b.symbol_expr->identifier() : irep_idt(); if(a_id.starts_with("java::java.lang.Object")) return false; diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 070f7282c1d..ec7a01fa037 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -63,7 +63,7 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) PRECONDITION(can_cast_expr(called_function_pointer)); auto const &pointer_symbol = to_symbol_expr(called_function_pointer); auto const restriction_iterator = - restrictions.restrictions.find(pointer_symbol.get_identifier()); + restrictions.restrictions.find(pointer_symbol.identifier()); if(restriction_iterator == restrictions.restrictions.end()) return false; @@ -348,7 +348,7 @@ static std::string resolve_pointer_name( auto const &called_function_pointer = to_dereference_expr(instruction.call_function()).pointer(); pointer_name = - id2string(to_symbol_expr(called_function_pointer).get_identifier()); + id2string(to_symbol_expr(called_function_pointer).identifier()); found = true; break; } @@ -450,8 +450,8 @@ function_pointer_restrictionst::get_by_name_restriction( const goto_programt::const_targett it = std::prev(location); INVARIANT( - to_symbol_expr(it->assign_lhs()).get_identifier() == - function_pointer_call_site.get_identifier(), + to_symbol_expr(it->assign_lhs()).identifier() == + function_pointer_call_site.identifier(), "called function pointer must have been assigned at the previous location"); if(!can_cast_expr(it->assign_rhs())) @@ -459,13 +459,13 @@ function_pointer_restrictionst::get_by_name_restriction( const auto &rhs = to_symbol_expr(it->assign_rhs()); - const auto restriction = by_name_restrictions.find(rhs.get_identifier()); + const auto restriction = by_name_restrictions.find(rhs.identifier()); if(restriction != by_name_restrictions.end()) { return std::optional( std::make_pair( - function_pointer_call_site.get_identifier(), restriction->second)); + function_pointer_call_site.identifier(), restriction->second)); } return {}; diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 05d9287e03c..a925a63f504 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -91,7 +91,7 @@ void slice_global_inits( if(!*seen_it && instruction.is_assign()) { const irep_idt id = - to_symbol_expr(instruction.assign_lhs()).get_identifier(); + to_symbol_expr(instruction.assign_lhs()).identifier(); // if we are to keep the left-hand side, then we also need to keep all // symbols occurring in the right-hand side diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 1c943021c11..6de670c1794 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -273,7 +273,7 @@ void string_abstractiont::declare_define_locals(goto_programt &dest) // same name may exist several times due to inlining, make sure the first // declaration is used available_decls.insert( - std::make_pair(it->decl_symbol().get_identifier(), it)); + std::make_pair(it->decl_symbol().identifier(), it)); // declare (and, if necessary, define) locals for(const auto &l : locals) @@ -1002,7 +1002,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write) bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest) { - const symbolt &symbol=ns.lookup(sym.get_identifier()); + const symbolt &symbol = ns.lookup(sym.identifier()); const typet &abstract_type=build_abstraction_type(symbol.type); CHECK_RETURN(!abstract_type.is_nil()); diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 2c44733b30d..53dc2266528 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -77,7 +77,7 @@ void validate_goto_modelt::check_called_functions() if(pointee.id() == ID_symbol && pointee.type().id() == ID_code) { - const auto &identifier = to_symbol_expr(pointee).get_identifier(); + const auto &identifier = to_symbol_expr(pointee).identifier(); DATA_CHECK( vm, @@ -108,7 +108,7 @@ void validate_goto_modelt::check_called_functions() "function call expected to be code-typed symbol expression"); const irep_idt &identifier = - to_symbol_expr(instr.call_function()).get_identifier(); + to_symbol_expr(instr.call_function()).identifier(); DATA_CHECK( vm, diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index aecd889d802..53e4833efb0 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -93,7 +93,7 @@ void output_vcd( auto lhs_object=step.get_lhs_object(); if(lhs_object.has_value()) { - irep_idt identifier=lhs_object->get_identifier(); + irep_idt identifier = lhs_object->identifier(); const typet &type=lhs_object->type(); const auto number=n.number(identifier); @@ -120,7 +120,7 @@ void output_vcd( auto lhs_object = step.get_lhs_object(); if(lhs_object.has_value()) { - irep_idt identifier = lhs_object->get_identifier(); + irep_idt identifier = lhs_object->identifier(); const typet &type = lhs_object->type(); out << '#' << timestamp << "\n"; diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index 6df7456db71..433c68db214 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -95,8 +95,7 @@ aliasingt aliasing( // the trivial case first if(e1.id()==ID_symbol && e2.id()==ID_symbol) { - if(to_symbol_expr(e1).get_identifier()== - to_symbol_expr(e2).get_identifier()) + if(to_symbol_expr(e1).identifier() == to_symbol_expr(e2).identifier()) return aliasingt::A_MUST; else return aliasingt::A_MUSTNOT; diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 446cf102059..68d3905771f 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -68,7 +68,7 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns) const auto &lhs_object = step.get_lhs_object(); const irep_idt identifier = - lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt(); + lhs_object.has_value() ? lhs_object->identifier() : irep_idt(); value_xml.data = get_printable_xml(ns, identifier, value); const auto &bv_type = type_try_dynamic_cast(value.type()); @@ -128,7 +128,7 @@ void convert( { auto lhs_object = step.get_lhs_object(); irep_idt identifier = - lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt(); + lhs_object.has_value() ? lhs_object->identifier() : irep_idt(); xmlt &xml_assignment = dest.new_element("assignment"); if(!xml_location.name.empty()) @@ -139,7 +139,7 @@ void convert( if( lhs_object.has_value() && - !ns.lookup(lhs_object->get_identifier(), symbol)) + !ns.lookup(lhs_object->identifier(), symbol)) { std::string type_string = from_type(ns, symbol->name, step.full_lhs.type()); diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index ead827225ea..57a72558537 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -88,8 +88,7 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state) if(symbol.base_name.starts_with("symex::auto_object")) { // done already? - if(!state.get_level2().current_names.has_key( - ssa_expr.get_identifier())) + if(!state.get_level2().current_names.has_key(ssa_expr.identifier())) { initialize_auto_object(e, state); } diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 0a5a56b6213..9b65ead1ae7 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -220,7 +220,7 @@ exprt field_sensitivityt::apply( // In case the array type was incomplete, attempt to retrieve it from // the symbol table. const symbolt *array_from_symbol_table = ns.get_symbol_table().lookup( - to_symbol_expr(index.array()).get_identifier()); + to_symbol_expr(index.array()).identifier()); if(array_from_symbol_table != nullptr) l2_size = to_array_type(array_from_symbol_table->type).size(); } @@ -373,7 +373,7 @@ void field_sensitivityt::field_assignments( // assignments, thus we cannot skip putting it in there above. if(is_divisible(lhs, true)) { - state.propagation.erase_if_exists(lhs.get_identifier()); + state.propagation.erase_if_exists(lhs.identifier()); state.value_set.erase_symbol(lhs, ns); } } @@ -419,7 +419,7 @@ void field_sensitivityt::field_assignments_rec( // assignments, thus we cannot skip putting it in there above. if(is_divisible(l1_lhs, true)) { - state.propagation.erase_if_exists(l1_lhs.get_identifier()); + state.propagation.erase_if_exists(l1_lhs.identifier()); state.value_set.erase_symbol(l1_lhs, ns); } } diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index 8cbe0038a13..64b704fd00c 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -105,7 +105,7 @@ void goto_statet::apply_condition( goto_symex_statet::write_is_shared_resultt::SHARED) { const ssa_exprt l1_lhs = remove_level_2(ssa_lhs); - const irep_idt &l1_identifier = l1_lhs.get_identifier(); + const irep_idt &l1_identifier = l1_lhs.identifier(); level2.increase_generation( l1_identifier, l1_lhs, previous_state.get_l2_name_provider()); diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 24d9e4dc33b..6b700ce09a6 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -91,7 +91,7 @@ void goto_symext::symex_assign( // Let's hide return value assignments. if( lhs.id() == ID_symbol && - id2string(to_symbol_expr(lhs).get_identifier()).find("#return_value!") != + id2string(to_symbol_expr(lhs).identifier()).find("#return_value!") != std::string::npos) { assignment_type = symex_targett::assignment_typet::HIDDEN; @@ -207,8 +207,7 @@ bool goto_symext::constant_propagate_assignment_with_side_effects( if(f_l1.function().id() == ID_symbol) { - const irep_idt &func_id = - to_symbol_expr(f_l1.function()).get_identifier(); + const irep_idt &func_id = to_symbol_expr(f_l1.function()).identifier(); if(func_id == ID_cprover_string_concat_func) { @@ -389,7 +388,7 @@ goto_symext::try_evaluate_constant_string( } const auto s_pointer_opt = - state.propagation.find(to_symbol_expr(content).get_identifier()); + state.propagation.find(to_symbol_expr(content).identifier()); if(!s_pointer_opt) { @@ -408,7 +407,7 @@ goto_symext::try_evaluate_constant(const statet &state, const exprt &expr) } const auto constant_expr_opt = - state.propagation.find(to_symbol_expr(expr).get_identifier()); + state.propagation.find(to_symbol_expr(expr).identifier()); if(!constant_expr_opt || !constant_expr_opt->get().is_constant()) { diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index a8bffc20bf3..13aa3f7d570 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -85,7 +85,7 @@ renamedt goto_symex_statet::assignment( { // identifier should be l0 or l1, make sure it's l1 lhs = rename_ssa(std::move(lhs), ns).get(); - irep_idt l1_identifier=lhs.get_identifier(); + irep_idt l1_identifier = lhs.identifier(); // the type might need renaming rename(lhs.type(), l1_identifier, ns); @@ -147,7 +147,7 @@ goto_symex_statet::rename_ssa(ssa_exprt ssa, const namespacet &ns) level == L0 || level == L1, "rename_ssa can only be used for levels L0 and L1"); ssa = set_indices(std::move(ssa), ns).get(); - rename(ssa.type(), ssa.get_identifier(), ns); + rename(ssa.type(), ssa.identifier(), ns); ssa.update_type(); return renamedt{ssa}; } @@ -187,7 +187,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) else { ssa = set_indices(std::move(ssa), ns).get(); - rename(expr.type(), ssa.get_identifier(), ns); + rename(expr.type(), ssa.identifier(), ns); ssa.update_type(); // renaming taken care of by l2_thread_encoding, or already at L2 @@ -206,7 +206,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) { // We also consider propagation if we go up to L2. // L1 identifiers are used for propagation! - auto p_it = propagation.find(ssa.get_identifier()); + auto p_it = propagation.find(ssa.identifier()); if(p_it.has_value()) { @@ -228,7 +228,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns) // we never rename function symbols if(type.id() == ID_code || type.id() == ID_mathematical_function) { - rename(expr.type(), to_symbol_expr(expr).get_identifier(), ns); + rename(expr.type(), to_symbol_expr(expr).identifier(), ns); return renamedt{std::move(expr)}; } else @@ -396,7 +396,7 @@ bool goto_symex_statet::l2_thread_read_encoding( return false; const ssa_exprt ssa_l1 = remove_level_2(expr); - const irep_idt &l1_identifier=ssa_l1.get_identifier(); + const irep_idt &l1_identifier = ssa_l1.identifier(); const exprt guard_as_expr = guard.as_expr(); // see whether we are within an atomic section @@ -449,7 +449,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // written this object within the atomic section. We must actually do this, // because goto_state::apply_condition may have placed the latest value in // the propagation map without recording an assignment. - auto p_it = propagation.find(ssa_l1.get_identifier()); + auto p_it = propagation.find(ssa_l1.identifier()); const exprt l2_true_case = p_it.has_value() ? *p_it : set_indices(ssa_l1, ns).get(); @@ -577,7 +577,7 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns) // only do L1! ssa = set_indices(std::move(ssa), ns).get(); - rename(expr.type(), ssa.get_identifier(), ns); + rename(expr.type(), ssa.identifier(), ns); ssa.update_type(); } else if(expr.id()==ID_symbol) @@ -809,7 +809,7 @@ ssa_exprt goto_symex_statet::add_object( framet &frame = call_stack().top(); const renamedt renamed = rename_ssa(ssa_exprt{expr}, ns); - const irep_idt l0_name = renamed.get_identifier(); + const irep_idt l0_name = renamed.identifier(); const std::size_t l1_index = index_generator(l0_name); if(const auto old_value = level1.insert_or_replace(renamed, l1_index)) @@ -820,7 +820,7 @@ ssa_exprt goto_symex_statet::add_object( } const ssa_exprt ssa = rename_ssa(renamed.get(), ns).get(); - const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second; + const bool inserted = frame.local_objects.insert(ssa.identifier()).second; INVARIANT(inserted, "l1_name expected to be unique by construction"); return ssa; @@ -828,7 +828,7 @@ ssa_exprt goto_symex_statet::add_object( ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns) { - const irep_idt &l1_identifier = ssa.get_identifier(); + const irep_idt &l1_identifier = ssa.identifier(); // rename type to L2 rename(ssa.type(), l1_identifier, ns); @@ -858,14 +858,14 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns) { const ssa_exprt &field_ssa = to_ssa_expr(*l1_symbol); const std::size_t field_generation = level2.increase_generation( - l1_symbol->get_identifier(), field_ssa, fresh_l2_name_provider); + l1_symbol->identifier(), field_ssa, fresh_l2_name_provider); CHECK_RETURN(field_generation == 1); } else if(auto fs_ssa = expr_try_dynamic_cast(e)) { const ssa_exprt &ssa = fs_ssa->get_object_ssa(); const std::size_t field_generation = level2.increase_generation( - ssa.get_identifier(), ssa, fresh_l2_name_provider); + ssa.identifier(), ssa, fresh_l2_name_provider); CHECK_RETURN(field_generation == 1); } }; diff --git a/src/goto-symex/partial_order_concurrency.h b/src/goto-symex/partial_order_concurrency.h index 3e48c8cfd1b..15e7d31dbac 100644 --- a/src/goto-symex/partial_order_concurrency.h +++ b/src/goto-symex/partial_order_concurrency.h @@ -85,7 +85,7 @@ class partial_order_concurrencyt /// \return identifier static inline irep_idt id(event_it event) { - return event->ssa_lhs.get_identifier(); + return event->ssa_lhs.identifier(); } /// Produce an address ID for an event @@ -93,7 +93,7 @@ class partial_order_concurrencyt /// \return L1-renamed identifier irep_idt address(event_it event) const { - return remove_level_2(event->ssa_lhs).get_identifier(); + return remove_level_2(event->ssa_lhs).identifier(); } typet clock_type; diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index cd3185aff42..5ac2bb6af42 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -158,7 +158,7 @@ bool postconditiont::is_used( } else if(expr.id()==ID_symbol) { - return to_symbol_expr(expr).get_identifier() == identifier; + return to_symbol_expr(expr).identifier() == identifier; } else if(expr.id()==ID_dereference) { diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index 7109f4b0c09..0f89e3cccfe 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -49,7 +49,7 @@ void symex_level1t::insert( std::size_t index) { current_names.insert( - ssa.get().get_identifier(), std::make_pair(ssa.get(), index)); + ssa.get().identifier(), std::make_pair(ssa.get(), index)); } std::optional> @@ -57,7 +57,7 @@ symex_level1t::insert_or_replace( const renamedt &ssa, std::size_t index) { - const irep_idt &identifier = ssa.get().get_identifier(); + const irep_idt &identifier = ssa.get().identifier(); const auto old_value = current_names.find(identifier); if(old_value) { @@ -71,7 +71,7 @@ symex_level1t::insert_or_replace( bool symex_level1t::has(const renamedt &ssa) const { - return current_names.has_key(ssa.get().get_identifier()); + return current_names.has_key(ssa.get().identifier()); } renamedt symex_level1t:: @@ -103,7 +103,7 @@ operator()(renamedt l1_expr) const { if(!l1_expr.get().get_level_2().empty()) return renamedt{std::move(l1_expr.value())}; - l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier())); + l1_expr.value().set_level_2(latest_index(l1_expr.get().identifier())); return renamedt{std::move(l1_expr.value())}; } diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index 5df8b64aee4..4d585fa8295 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -58,7 +58,7 @@ void shadow_memoryt::initialize_shadow_memory( } log.debug() << "Shadow memory: initialize field " - << id2string(shadow.get_identifier()) << " for " << format(expr) + << id2string(shadow.identifier()) << " for " << format(expr) << " with initial value " << format(field_pair.second) << messaget::eom; } @@ -348,7 +348,7 @@ void shadow_memoryt::symex_field_static_init( return; const irep_idt &identifier = - to_symbol_expr(lhs.get_original_expr()).get_identifier(); + to_symbol_expr(lhs.get_original_expr()).identifier(); if(state.source.function_id != INITIALIZE_FUNCTION) return; @@ -386,7 +386,7 @@ void shadow_memoryt::symex_field_static_init_string_constant( if( expr.get_original_expr().id() == ID_symbol && to_symbol_expr(expr.get_original_expr()) - .get_identifier() + .identifier() .starts_with(CPROVER_PREFIX)) { return; @@ -408,7 +408,7 @@ void shadow_memoryt::symex_field_local_init( const ssa_exprt &expr) { const symbolt &symbol = - ns.lookup(to_symbol_expr(expr.get_original_expr()).get_identifier()); + ns.lookup(to_symbol_expr(expr.get_original_expr()).identifier()); const std::string symbol_name = id2string(symbol.name); if( @@ -439,7 +439,7 @@ void shadow_memoryt::symex_field_local_init( const typet &type = expr.type(); ssa_exprt expr_l1 = remove_level_2(expr); log.debug() << "Shadow memory: local memory " - << id2string(expr_l1.get_identifier()) << " of type " + << id2string(expr_l1.identifier()) << " of type " << from_type(ns, "", type) << messaget::eom; initialize_shadow_memory( @@ -479,7 +479,7 @@ shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations( if(function.id() != ID_symbol) continue; - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); if( identifier == diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index 4bd18bf3046..bc1d1ed1476 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -282,9 +282,9 @@ void replace_invalid_object_by_null(exprt &expr) { if( expr.id() == ID_symbol && expr.type().id() == ID_pointer && - (id2string(to_symbol_expr(expr).get_identifier()).rfind("invalid_object") != + (id2string(to_symbol_expr(expr).identifier()).rfind("invalid_object") != std::string::npos || - id2string(to_symbol_expr(expr).get_identifier()).rfind("$object") != + id2string(to_symbol_expr(expr).identifier()).rfind("$object") != std::string::npos)) { expr = null_pointer_exprt(to_pointer_type(expr.type())); diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index edb2821fc89..ddbe1df4053 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -104,7 +104,7 @@ void symex_slicet::slice(SSA_stept &SSA_step) void symex_slicet::slice_assignment(SSA_stept &SSA_step) { PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol); - const irep_idt &id=SSA_step.ssa_lhs.get_identifier(); + const irep_idt &id = SSA_step.ssa_lhs.identifier(); auto entry = depends.find(id); if(entry == depends.end()) @@ -122,7 +122,7 @@ void symex_slicet::slice_assignment(SSA_stept &SSA_step) void symex_slicet::slice_decl(SSA_stept &SSA_step) { - const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier(); + const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).identifier(); if(depends.find(id)==depends.end()) { @@ -170,7 +170,7 @@ void symex_slicet::collect_open_variables( case goto_trace_stept::typet::ASSIGNMENT: get_symbols(SSA_step.ssa_rhs); - lhs.insert(SSA_step.ssa_lhs.get_identifier()); + lhs.insert(SSA_step.ssa_lhs.identifier()); break; case goto_trace_stept::typet::OUTPUT: diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp index 231c40303e7..4900b8d34ec 100644 --- a/src/goto-symex/symex_atomic_section.cpp +++ b/src/goto-symex/symex_atomic_section.cpp @@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state) for(const auto &pair : state.written_in_atomic_section) { ssa_exprt w = pair.first; - w.set_level_2(state.get_level2().latest_index(w.get_identifier())); + w.set_level_2(state.get_level2().latest_index(w.identifier())); // guard is the disjunction over writes PRECONDITION(!pair.second.empty()); diff --git a/src/goto-symex/symex_dead.cpp b/src/goto-symex/symex_dead.cpp index d373a46525a..dfc7a769286 100644 --- a/src/goto-symex/symex_dead.cpp +++ b/src/goto-symex/symex_dead.cpp @@ -27,7 +27,7 @@ static void remove_l1_object_rec( if(is_ssa_expr(l1_expr)) { const ssa_exprt &l1_ssa = to_ssa_expr(l1_expr); - const irep_idt &l1_identifier = l1_ssa.get_identifier(); + const irep_idt &l1_identifier = l1_ssa.identifier(); // We cannot remove the object from the L1 renaming map, because L1 renaming // information is not local to a path, but removing it from the propagation diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index aff5c9b82cd..a33352d2b83 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -40,7 +40,7 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) // we hide the declaration of auxiliary variables // and if the statement itself is hidden - bool hidden = ns.lookup(expr.get_identifier()).is_auxiliary || + bool hidden = ns.lookup(expr.identifier()).is_auxiliary || state.call_stack().top().hidden_function || state.source.pc->source_location().get_hide(); diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp index 835256d91f2..297ee35d3c3 100644 --- a/src/goto-symex/symex_dereference_state.cpp +++ b/src/goto-symex/symex_dereference_state.cpp @@ -46,15 +46,14 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr) symbolt *sym_ptr=nullptr; const ssa_exprt sym_expr = state.rename_ssa(ssa_exprt{sym.symbol_expr()}, ns).get(); - sym.name = sym_expr.get_identifier(); + sym.name = sym_expr.identifier(); state.symbol_table.move(sym, sym_ptr); return sym_ptr; } } else if(expr.id()==ID_symbol) { - const symbolt &ptr_symbol= - ns.lookup(to_symbol_expr(expr).get_identifier()); + const symbolt &ptr_symbol = ns.lookup(to_symbol_expr(expr).identifier()); const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol); @@ -65,7 +64,7 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr) symbolt *sym_ptr=nullptr; const ssa_exprt sym_expr = state.rename_ssa(ssa_exprt{sym.symbol_expr()}, ns).get(); - sym.name = sym_expr.get_identifier(); + sym.name = sym_expr.identifier(); state.symbol_table.move(sym, sym_ptr); return sym_ptr; } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index db4bfa133bc..a23c6a7b426 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -214,7 +214,7 @@ void goto_symext::symex_function_call_symbol( target.location(state.guard.as_expr(), state.source); PRECONDITION(function.id() == ID_symbol); - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).identifier(); if(identifier == CPROVER_PREFIX SHADOW_MEMORY_GET_FIELD) { @@ -240,7 +240,7 @@ void goto_symext::symex_function_call_post_clean( const symbol_exprt &function, const exprt::operandst &cleaned_arguments) { - const irep_idt &identifier = function.get_identifier(); + const irep_idt &identifier = function.identifier(); const goto_functionst::goto_functiont &goto_function = get_goto_function(identifier); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 3bde290706b..9092c3f5989 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -339,10 +339,11 @@ void goto_symext::symex_goto(statet &state) log.conditional_output( log.debug(), - [this, &new_lhs](messaget::mstreamt &mstream) { - mstream << "Assignment to " << new_lhs.get_identifier() - << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]" - << messaget::eom; + [this, &new_lhs](messaget::mstreamt &mstream) + { + mstream << "Assignment to " << new_lhs.identifier() << " [" + << pointer_offset_bits(new_lhs.type(), ns).value_or(0) + << " bits]" << messaget::eom; }); target.assignment( @@ -583,7 +584,7 @@ static void merge_names( const std::size_t goto_count, const std::size_t dest_count) { - const irep_idt l1_identifier = ssa.get_identifier(); + const irep_idt l1_identifier = ssa.identifier(); const irep_idt &obj_identifier = ssa.get_object_name(); if(obj_identifier == goto_symext::statet::guard_identifier()) @@ -682,8 +683,10 @@ static void merge_names( dest_state.record_events.pop(); log.conditional_output( - log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) { - mstream << "Assignment to " << new_lhs.get_identifier() << " [" + log.debug(), + [ns, &new_lhs](messaget::mstreamt &mstream) + { + mstream << "Assignment to " << new_lhs.identifier() << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]" << messaget::eom; }); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index a6ca641f16e..9e9e519a68a 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -868,14 +868,14 @@ void goto_symext::try_filter_value_sets( if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty()) { auto entry_index = jump_taken_value_set->get_index_of_symbol( - symbol_expr->get_identifier(), symbol_type, "", ns); + symbol_expr->identifier(), symbol_type, "", ns); jump_taken_value_set->erase_values_from_entry( *entry_index, erase_from_jump_taken_value_set); } if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty()) { auto entry_index = jump_not_taken_value_set->get_index_of_symbol( - symbol_expr->get_identifier(), symbol_type, "", ns); + symbol_expr->identifier(), symbol_type, "", ns); jump_not_taken_value_set->erase_values_from_entry( *entry_index, erase_from_jump_not_taken_value_set); } diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index a394209c413..63bcaac472e 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -76,7 +76,7 @@ void goto_symext::symex_start_thread(statet &state) // get L0 name for current thread const renamedt l0_lhs = symex_level0(std::move(lhs), ns, new_thread_nr); - const irep_idt &l0_name = l0_lhs.get().get_identifier(); + const irep_idt &l0_name = l0_lhs.get().identifier(); std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0); CHECK_RETURN(l1_index == 0); diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 9214c70608e..fee949e2546 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -46,7 +46,7 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix) { if( it->id() == ID_symbol && - to_symbol_expr(*it).get_identifier().starts_with(prefix)) + to_symbol_expr(*it).identifier().starts_with(prefix)) { return true; } @@ -416,7 +416,7 @@ cext cegis_verifiert::build_cex( expr_try_dynamic_cast(step.full_lhs); // malloc_size is not-hidden tmp variable. - if(id2string(symbol->get_identifier()) != "malloc::malloc_size") + if(id2string(symbol->identifier()) != "malloc::malloc_size") { live_variables.emplace(step.full_lhs); } diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index f1f878c058b..d1bdd3140ed 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -166,7 +166,7 @@ void enumerative_loop_contracts_synthesizert::init_candidates() if(auto symbol_expr = expr_try_dynamic_cast(*it)) { if(has_prefix( - id2string(symbol_expr->get_identifier()), CPROVER_PREFIX)) + id2string(symbol_expr->identifier()), CPROVER_PREFIX)) { it = assigns_map[new_id].erase(it); continue; @@ -246,7 +246,7 @@ void enumerative_loop_contracts_synthesizert::build_tmp_post_map() // tmp_post variables have identifiers with the prefix tmp::tmp_post. if( - id2string(symbol_lhs->get_identifier()).find("tmp::tmp_post") != + id2string(symbol_lhs->identifier()).find("tmp::tmp_post") != std::string::npos) { tmp_post_map[instruction.assign_lhs()] = instruction.assign_rhs(); @@ -272,7 +272,7 @@ enumerative_loop_contracts_synthesizert::compute_dependent_symbols( // the original symbol table. for(auto it = result.begin(); it != result.end();) { - if(original_symbol_table.lookup(it->get_identifier()) == nullptr) + if(original_symbol_table.lookup(it->identifier()) == nullptr) { it = result.erase(it); } diff --git a/src/linking/casting_replace_symbol.cpp b/src/linking/casting_replace_symbol.cpp index b0872400002..5e099092b52 100644 --- a/src/linking/casting_replace_symbol.cpp +++ b/src/linking/casting_replace_symbol.cpp @@ -82,7 +82,7 @@ bool casting_replace_symbolt::replace(exprt &dest) const bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const { - expr_mapt::const_iterator it = expr_map.find(s.get_identifier()); + expr_mapt::const_iterator it = expr_map.find(s.identifier()); if(it == expr_map.end()) return true; diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 645ec3c2725..2b498a837b8 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -193,7 +193,7 @@ symbol_tablet gdb_value_extractort::get_snapshot_as_symbol_table() for(const auto &pair : assignments) { const symbol_exprt &symbol_expr = to_symbol_expr(pair.first); - const irep_idt id = symbol_expr.get_identifier(); + const irep_idt id = symbol_expr.identifier(); INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table"); @@ -455,8 +455,8 @@ exprt gdb_value_extractort::get_non_char_pointer_value( return known_value; if(known_value.is_not_nil() && known_value.type() != expected_type) { - return symbol_exprt{to_symbol_expr(known_value).get_identifier(), - expected_type}; + return symbol_exprt{ + to_symbol_expr(known_value).identifier(), expected_type}; } return known_value; } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 3641c00fd60..aad9ae75f69 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -562,7 +562,7 @@ void value_sett::get_value_set_rec( ? remove_level_2(to_ssa_expr(expr)) : to_symbol_expr(expr); auto entry_index = - get_index_of_symbol(expr_l1.get_identifier(), expr.type(), suffix, ns); + get_index_of_symbol(expr_l1.identifier(), expr.type(), suffix, ns); if(entry_index.has_value()) make_union(dest, find_entry(*entry_index)->object_map); @@ -1675,7 +1675,7 @@ void value_sett::assign_rec( { const symbol_exprt lhs_l1 = is_ssa_expr(lhs) ? remove_level_2(to_ssa_expr(lhs)) : to_symbol_expr(lhs); - const irep_idt &identifier = lhs_l1.get_identifier(); + const irep_idt &identifier = lhs_l1.identifier(); update_entry( entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets); @@ -2071,6 +2071,5 @@ void value_sett::erase_symbol( const symbol_exprt &symbol_expr, const namespacet &ns) { - erase_symbol_rec( - symbol_expr.type(), id2string(symbol_expr.get_identifier()), ns); + erase_symbol_rec(symbol_expr.type(), id2string(symbol_expr.identifier()), ns); } diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 1e949add1e4..7a57fdad707 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -461,7 +461,7 @@ void value_set_fit::get_value_set_rec( { // just keep a reference to the ident in the set // (if it exists) - irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix; + irep_idt ident = id2string(to_symbol_expr(expr).identifier()) + suffix; valuest::const_iterator v_it=values.find(ident); if(ident.starts_with(alloc_adapter_prefix)) @@ -1208,7 +1208,7 @@ void value_set_fit::assign_rec( } else if(lhs.id()==ID_symbol) { - const irep_idt &identifier = to_symbol_expr(lhs).get_identifier(); + const irep_idt &identifier = to_symbol_expr(lhs).identifier(); if( identifier.starts_with("value_set::dynamic_object") || diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 96cb3c8045f..36041ad6ff7 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -94,7 +94,7 @@ void arrayst::collect_indices(const exprt &expr) { if(expr.id() == ID_array_comprehension) array_comprehension_args.insert( - to_array_comprehension_expr(expr).arg().get_identifier()); + to_array_comprehension_expr(expr).arg().identifier()); for(const auto &op : expr.operands()) collect_indices(op); @@ -105,8 +105,8 @@ void arrayst::collect_indices(const exprt &expr) if( e.index().id() == ID_symbol && - array_comprehension_args.count( - to_symbol_expr(e.index()).get_identifier()) != 0) + array_comprehension_args.count(to_symbol_expr(e.index()).identifier()) != + 0) { return; } diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 3cbeca98a76..88b2d69692c 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -511,8 +511,7 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) const bvt &bv1=convert_bv(expr.rhs()); - const irep_idt &identifier= - to_symbol_expr(expr.lhs()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr.lhs()).identifier(); map.set_literals(identifier, type, bv1); @@ -564,7 +563,7 @@ binding_exprt::variablest boolbvt::fresh_binding(const binding_exprt &binding) for(const auto &binding : binding.variables()) { - const auto &old_identifier = binding.get_identifier(); + const auto &old_identifier = binding.identifier(); // produce a new identifier const irep_idt new_identifier = diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp index 554dfda740f..177832db230 100644 --- a/src/solvers/flattening/boolbv_let.cpp +++ b/src/solvers/flattening/boolbv_let.cpp @@ -51,7 +51,7 @@ bvt boolbvt::convert_let(const let_exprt &expr) // Now assign for(const auto &binding : make_range(fresh_variables).zip(converted_values)) { - const auto &identifier = binding.first.get_identifier(); + const auto &identifier = binding.first.identifier(); // make the symbol visible if(binding.first.is_boolean()) @@ -81,9 +81,9 @@ bvt boolbvt::convert_let(const let_exprt &expr) { const auto &type = entry.type(); if(type.id() == ID_bool) - symbols.erase(entry.get_identifier()); + symbols.erase(entry.identifier()); else - map.erase_literals(entry.get_identifier(), type); + map.erase_literals(entry.identifier(), type); } return result_bv; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b52c0da27f9..52482e8b060 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -381,7 +381,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) if(expr.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(expr).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr).identifier(); return map.get_literals(identifier, type, bits); } diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index dcd3ae01b40..79f487fdcc6 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -27,7 +27,7 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const return expr.type().get_bool(ID_C_dynamic) || (expr.id() == ID_symbol && has_prefix( - id2string(to_symbol_expr(expr).get_identifier()), + id2string(to_symbol_expr(expr).identifier()), SYMEX_DYNAMIC_PREFIX "::")); } diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 505e450a150..575fdfc6565 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -89,7 +89,7 @@ std::optional prop_conv_solvert::get_bool(const exprt &expr) const else if(expr.id() == ID_symbol) { symbolst::const_iterator result = - symbols.find(to_symbol_expr(expr).get_identifier()); + symbols.find(to_symbol_expr(expr).identifier()); // This may fail if the symbol isn't Boolean or // not in the formula. @@ -207,7 +207,7 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) } else if(expr.id() == ID_symbol) { - return get_literal(to_symbol_expr(expr).get_identifier()); + return get_literal(to_symbol_expr(expr).identifier()); } else if(expr.id() == ID_literal) { @@ -328,7 +328,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr) if(expr.lhs().id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier(); + const irep_idt &identifier = to_symbol_expr(expr.lhs()).identifier(); literalt tmp = convert(expr.rhs()); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 92c61e1a1c7..72cc98d0499 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -339,7 +339,7 @@ exprt smt2_convt::get(const exprt &expr) const { if(expr.id()==ID_symbol) { - const irep_idt &id=to_symbol_expr(expr).get_identifier(); + const irep_idt &id = to_symbol_expr(expr).identifier(); identifier_mapt::const_iterator it=identifier_map.find(id); @@ -1207,7 +1207,7 @@ void smt2_convt::convert_floatbv(const exprt &expr) if(expr.id()==ID_symbol) { - const irep_idt &id = to_symbol_expr(expr).get_identifier(); + const irep_idt &id = to_symbol_expr(expr).identifier(); out << convert_identifier(id); return; } @@ -1261,7 +1261,7 @@ void smt2_convt::convert_expr(const exprt &expr) // huge monster case split over expression id if(expr.id()==ID_symbol) { - const irep_idt &id = to_symbol_expr(expr).get_identifier(); + const irep_idt &id = to_symbol_expr(expr).identifier(); DATA_INVARIANT(!id.empty(), "symbol must have identifier"); out << convert_identifier(id); } @@ -1883,7 +1883,7 @@ void smt2_convt::convert_expr(const exprt &expr) out << "(! "; convert(named_term_expr.value()); out << " :named " - << convert_identifier(named_term_expr.symbol().get_identifier()) << ')'; + << convert_identifier(named_term_expr.symbol().identifier()) << ')'; } else if(expr.id()==ID_with) { @@ -5056,8 +5056,8 @@ void smt2_convt::set_to(const exprt &expr, bool value) if(equal_expr.lhs().id()==ID_symbol) { - const irep_idt &identifier= - to_symbol_expr(equal_expr.lhs()).get_identifier(); + const irep_idt &identifier = + to_symbol_expr(equal_expr.lhs()).identifier(); if( identifier_map.find(identifier) == identifier_map.end() && @@ -5260,7 +5260,7 @@ void smt2_convt::find_symbols(const exprt &expr) const auto &q_expr = to_quantifier_expr(expr); for(const auto &symbol : q_expr.variables()) { - const auto identifier = symbol.get_identifier(); + const auto identifier = symbol.identifier(); auto id_entry = identifier_map.insert({identifier, identifiert{symbol.type(), true}}); shadowed_syms.insert( @@ -5294,7 +5294,7 @@ void smt2_convt::find_symbols(const exprt &expr) irep_idt identifier; if(expr.id()==ID_symbol) - identifier=to_symbol_expr(expr).get_identifier(); + identifier = to_symbol_expr(expr).identifier(); else identifier="nondet_"+ id2string(to_nondet_symbol_expr(expr).get_identifier()); diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index 0bdca09dfc4..d54826e7342 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -126,7 +126,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) } else if(expr.id() == ID_symbol) { - const auto &identifier = to_symbol_expr(expr).get_identifier(); + const auto &identifier = to_symbol_expr(expr).identifier(); if(expr.get_bool("#quoted")) { out << '|'; diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index f7952e56fb5..02710085339 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -249,7 +249,7 @@ std::pair smt2_parsert::binding(irep_idt id) for(auto &b : bindings) { auto insert_result = - id_map.insert({b.get_identifier(), idt{idt::BINDING, b.type()}}); + id_map.insert({b.identifier(), idt{idt::BINDING, b.type()}}); if(!insert_result.second) // already there { auto &id_entry = *insert_result.first; @@ -266,7 +266,7 @@ std::pair smt2_parsert::binding(irep_idt id) // remove bindings from id_map for(const auto &b : bindings) - id_map.erase(b.get_identifier()); + id_map.erase(b.identifier()); // restore any previous ids for(auto &saved_id : saved_ids) @@ -565,7 +565,7 @@ exprt smt2_parsert::function_application() const symbol_exprt symbol_expr( smt2_tokenizer.get_buffer(), bool_typet()); named_terms.emplace( - symbol_expr.get_identifier(), named_termt(term, symbol_expr)); + symbol_expr.identifier(), named_termt(term, symbol_expr)); } else throw error("invalid name attribute, expected symbol"); diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index 73e1617e13d..9d0652f7989 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -83,7 +83,7 @@ void smt2_solvert::expand_function_applications(exprt &expr) if(app.function().id() == ID_symbol) { // look up the symbol - auto identifier = to_symbol_expr(app.function()).get_identifier(); + auto identifier = to_symbol_expr(app.function()).identifier(); auto f_it = id_map.find(identifier); if(f_it != id_map.end()) @@ -231,7 +231,7 @@ void smt2_solvert::setup_commands() if(op.id() != ID_symbol) throw error("get-value expects symbol"); - const auto &identifier = to_symbol_expr(op).get_identifier(); + const auto &identifier = to_symbol_expr(op).identifier(); const auto id_map_it = id_map.find(identifier); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..c08ea2b6fb1 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -115,8 +115,8 @@ smt_sortt convert_type_to_smt_sort(const typet &type) static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr) { - return smt_identifier_termt{symbol_expr.get_identifier(), - convert_type_to_smt_sort(symbol_expr.type())}; + return smt_identifier_termt{ + symbol_expr.identifier(), convert_type_to_smt_sort(symbol_expr.type())}; } static smt_termt convert_expr_to_smt( diff --git a/src/solvers/smt2_incremental/object_tracking.cpp b/src/solvers/smt2_incremental/object_tracking.cpp index e9571d08b1b..1c5ae0d83d3 100644 --- a/src/solvers/smt2_incremental/object_tracking.cpp +++ b/src/solvers/smt2_incremental/object_tracking.cpp @@ -92,7 +92,7 @@ static bool is_dynamic(const exprt &object) return true; const auto symbol = expr_try_dynamic_cast(object); bool symbol_is_dynamic = - symbol && symbol->get_identifier().starts_with(SYMEX_DYNAMIC_PREFIX); + symbol && symbol->identifier().starts_with(SYMEX_DYNAMIC_PREFIX); return symbol_is_dynamic; } diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0d8a91a6f89..0dbf7ae8616 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -211,7 +211,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( { send_function_definition( *symbol_expr, - symbol_expr->get_identifier(), + symbol_expr->identifier(), solver_process, expression_identifiers, identifier_table); diff --git a/src/solvers/strings/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h index d515c7f4652..fdcab8ade1b 100644 --- a/src/solvers/strings/string_builtin_function.h +++ b/src/solvers/strings/string_builtin_function.h @@ -428,7 +428,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont { PRECONDITION(function_application.function().id() == ID_symbol); return id2string( - to_symbol_expr(function_application.function()).get_identifier()); + to_symbol_expr(function_application.function()).identifier()); } std::vector string_arguments() const override { diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 81603410ed6..2b597837244 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -189,7 +189,7 @@ static irep_idt get_function_name(const function_application_exprt &expr) const exprt &name = expr.function(); PRECONDITION(name.id() == ID_symbol); PRECONDITION(!is_ssa_expr(name)); - return to_symbol_expr(name).get_identifier(); + return to_symbol_expr(name).identifier(); } std::optional diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index 039557734a1..fb2b2f5d42a 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -489,7 +489,7 @@ std::pair string_constraint_generatort::add_axioms_for_is_valid_int( const function_application_exprt &f) { - irep_idt called_function = to_symbol_expr(f.function()).get_identifier(); + irep_idt called_function = to_symbol_expr(f.function()).identifier(); PRECONDITION( called_function == ID_cprover_string_is_valid_int_func || called_function == ID_cprover_string_is_valid_long_func); diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp index 17a5105c8f8..833f08c91e9 100644 --- a/src/solvers/strings/string_dependencies.cpp +++ b/src/solvers/strings/string_dependencies.cpp @@ -30,7 +30,7 @@ static std::unique_ptr to_string_builtin_function( const auto name = expr_checked_cast(fun_app.function()); PRECONDITION(!is_ssa_expr(name)); - const irep_idt &id = name.get_identifier(); + const irep_idt &id = name.identifier(); if(id == ID_cprover_string_insert_func) return std::make_unique( diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 0b7bd009e4b..7af950d095a 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -1145,8 +1145,8 @@ void debug_model( for(const auto &symbol : symbols) { - stream << " - " << symbol.get_identifier() << ": " - << format(super_get(symbol)) << '\n'; + stream << " - " << symbol.identifier() << ": " << format(super_get(symbol)) + << '\n'; } stream << messaget::eom; } @@ -1451,7 +1451,7 @@ static std::pair> check_axioms( ns, negated_axiom, univ_var, stream.message.get_message_handler())) { stream << std::string(4, ' ') - << "- violated_for: " << univ_var.get_identifier() << "=" + << "- violated_for: " << univ_var.identifier() << "=" << format(*witness) << messaget::eom; violated_not_contains[i] = *witness; } diff --git a/src/statement-list/converters/expr2statement_list.cpp b/src/statement-list/converters/expr2statement_list.cpp index fce51c9dcc2..6c0dae703fe 100644 --- a/src/statement-list/converters/expr2statement_list.cpp +++ b/src/statement-list/converters/expr2statement_list.cpp @@ -211,7 +211,7 @@ void expr2stlt::convert(const symbol_exprt &expr) result << REFERENCE_FLAG; is_reference = false; } - result << id2string(id_shorthand(expr.get_identifier())); + result << id2string(id_shorthand(expr.identifier())); } void expr2stlt::convert_multiary_bool( diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp index 91dee4ec54b..f24cb2f92df 100644 --- a/src/statement-list/statement_list_parse_tree_io.cpp +++ b/src/statement-list/statement_list_parse_tree_io.cpp @@ -238,7 +238,7 @@ void output_instruction( expr_try_dynamic_cast(expr); if(symbol) { - os << '\t' << symbol->get_identifier(); + os << '\t' << symbol->identifier(); continue; } const constant_exprt *const constant = diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index e91f45ba535..f8ecf3a3fe2 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -226,7 +226,7 @@ void statement_list_typecheckt::typecheck_tag_list() { for(const symbol_exprt &tag : parse_tree.tags) { - symbolt tag_sym{tag.get_identifier(), tag.type(), ID_statement_list}; + symbolt tag_sym{tag.identifier(), tag.type(), ID_statement_list}; tag_sym.is_static_lifetime = true; tag_sym.module = module; tag_sym.base_name = tag_sym.name; @@ -269,7 +269,7 @@ void statement_list_typecheckt::typecheck_function_block_var_decls( for(const statement_list_parse_treet::var_declarationt &declaration : var_decls) { - const irep_idt &var_name{declaration.variable.get_identifier()}; + const irep_idt &var_name{declaration.variable.identifier()}; const typet &var_type{declaration.variable.type()}; struct_union_typet::componentt component{var_name, var_type}; component.set(ID_statement_list_type, var_property); @@ -290,15 +290,15 @@ void statement_list_typecheckt::typecheck_function_var_decls( param_sym.module = module; param_sym.type = declaration.variable.type(); param_sym.name = id2string(function_name) + - "::" + id2string(declaration.variable.get_identifier()); - param_sym.base_name = declaration.variable.get_identifier(); + "::" + id2string(declaration.variable.identifier()); + param_sym.base_name = declaration.variable.identifier(); param_sym.pretty_name = param_sym.base_name; param_sym.mode = ID_statement_list; symbol_table.add(param_sym); code_typet::parametert param{declaration.variable.type()}; param.set_identifier(param_sym.name); - param.set_base_name(declaration.variable.get_identifier()); + param.set_base_name(declaration.variable.identifier()); param.set(ID_statement_list_type, var_property); params.push_back(param); } @@ -313,10 +313,10 @@ void statement_list_typecheckt::typecheck_temp_var_decls( { symbolt temp_sym{ id2string(tia_symbol.name) + - "::" + id2string(declaration.variable.get_identifier()), + "::" + id2string(declaration.variable.identifier()), declaration.variable.type(), ID_statement_list}; - temp_sym.base_name = declaration.variable.get_identifier(); + temp_sym.base_name = declaration.variable.identifier(); temp_sym.pretty_name = temp_sym.base_name; temp_sym.module = module; symbol_table.add(temp_sym); @@ -631,7 +631,7 @@ void statement_list_typecheckt::typecheck_statement_list_load( expr_try_dynamic_cast(op_code.op0()); if(symbol) { - const irep_idt &identifier{symbol->get_identifier()}; + const irep_idt &identifier{symbol->identifier()}; const exprt val{typecheck_identifier(tia_element, identifier)}; accumulator.push_back(val); } @@ -649,7 +649,7 @@ void statement_list_typecheckt::typecheck_statement_list_transfer( symbolt &tia_element) { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; - const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())}; + const exprt lhs{typecheck_identifier(tia_element, op.identifier())}; if(lhs.type() != accumulator.back().type()) { error() << "Types of transfer assignment do not match" << eom; @@ -1004,7 +1004,7 @@ void statement_list_typecheckt::typecheck_statement_list_or( } const symbol_exprt &sym{ typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const exprt op{typecheck_identifier(tia_element, sym.identifier())}; // If inside of a bit string, create an 'or' expression with the operand and // the current contents of the rlo bit. @@ -1024,7 +1024,7 @@ void statement_list_typecheckt::typecheck_statement_list_or_not( { const symbol_exprt &sym{ typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const exprt op{typecheck_identifier(tia_element, sym.identifier())}; const not_exprt not_op{op}; // If inside of a bit string, create an 'or' expression with the operand and @@ -1045,7 +1045,7 @@ void statement_list_typecheckt::typecheck_statement_list_xor( { const symbol_exprt &sym{ typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const exprt op{typecheck_identifier(tia_element, sym.identifier())}; // If inside of a bit string, create an 'xor' expression with the operand and // the current contents of the rlo bit. @@ -1065,7 +1065,7 @@ void statement_list_typecheckt::typecheck_statement_list_xor_not( { const symbol_exprt &sym{ typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const exprt op{typecheck_identifier(tia_element, sym.identifier())}; const not_exprt not_op{op}; // If inside of a bit string, create an 'xor not' expression with the @@ -1203,7 +1203,7 @@ void statement_list_typecheckt::typecheck_statement_list_assign( symbolt &tia_element) { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; - const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())}; + const exprt lhs{typecheck_identifier(tia_element, op.identifier())}; if(lhs.type() != rlo_bit.type()) { @@ -1242,7 +1242,7 @@ void statement_list_typecheckt::typecheck_statement_list_set( symbolt &tia_element) { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; - const irep_idt &identifier{op.get_identifier()}; + const irep_idt &identifier{op.identifier()}; save_rlo_state(tia_element); @@ -1259,7 +1259,7 @@ void statement_list_typecheckt::typecheck_statement_list_reset( symbolt &tia_element) { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; - const irep_idt &identifier{op.get_identifier()}; + const irep_idt &identifier{op.identifier()}; save_rlo_state(tia_element); @@ -1276,7 +1276,7 @@ void statement_list_typecheckt::typecheck_statement_list_call( symbolt &tia_element) { const symbol_exprt &op{typecheck_instruction_with_non_const_operand(op_code)}; - const irep_idt &identifier{op.get_identifier()}; + const irep_idt &identifier{op.identifier()}; if(symbol_table.has_symbol(identifier)) typecheck_called_tia_element(op_code, tia_element); else if(identifier == CPROVER_ASSUME) @@ -1298,10 +1298,10 @@ void statement_list_typecheckt::typecheck_statement_list_jump_unconditional( { const symbol_exprt &label{ typecheck_instruction_with_non_const_operand(op_code)}; - typecheck_label_reference(label.get_identifier(), false); + typecheck_label_reference(label.identifier(), false); save_rlo_state(tia_element); - code_gotot unconditional{label.get_identifier()}; + code_gotot unconditional{label.identifier()}; tia_element.value.add_to_operands(unconditional); } @@ -1311,10 +1311,10 @@ void statement_list_typecheckt::typecheck_statement_list_jump_conditional( { const symbol_exprt &label{ typecheck_instruction_with_non_const_operand(op_code)}; - typecheck_label_reference(label.get_identifier(), true); + typecheck_label_reference(label.identifier(), true); save_rlo_state(tia_element); - code_gotot jump{label.get_identifier()}; + code_gotot jump{label.identifier()}; code_ifthenelset conditional{rlo_bit, jump}; tia_element.value.add_to_operands(conditional); @@ -1329,10 +1329,10 @@ void statement_list_typecheckt::typecheck_statement_list_jump_conditional_not( { const symbol_exprt &label{ typecheck_instruction_with_non_const_operand(op_code)}; - typecheck_label_reference(label.get_identifier(), true); + typecheck_label_reference(label.identifier(), true); save_rlo_state(tia_element); - code_gotot jump{label.get_identifier()}; + code_gotot jump{label.identifier()}; code_ifthenelset not_conditional{not_exprt{rlo_bit}, jump}; tia_element.value.add_to_operands(not_conditional); @@ -1513,7 +1513,7 @@ exprt statement_list_typecheckt::typecheck_simple_boolean_instruction_operand( { const symbol_exprt &sym{ typecheck_instruction_with_non_const_operand(op_code)}; - const exprt op{typecheck_identifier(tia_element, sym.get_identifier())}; + const exprt op{typecheck_identifier(tia_element, sym.identifier())}; const not_exprt not_op{op}; return negate ? not_op : op; } @@ -1624,7 +1624,7 @@ void statement_list_typecheckt::typecheck_called_tia_element( { const symbol_exprt &call_operand{to_symbol_expr(op_code.op0())}; const symbolt &called_function{ - symbol_table.lookup_ref(call_operand.get_identifier())}; + symbol_table.lookup_ref(call_operand.identifier())}; const code_typet &called_type{to_code_type(called_function.type)}; // Is it a STL function or STL function block? if( @@ -1646,7 +1646,7 @@ void statement_list_typecheckt::typecheck_called_function( { const symbol_exprt call_operand{to_symbol_expr(op_code.op0())}; const symbolt &called_function_sym{ - symbol_table.lookup_ref(call_operand.get_identifier())}; + symbol_table.lookup_ref(call_operand.identifier())}; const symbol_exprt called_function_expr{called_function_sym.symbol_expr()}; const code_typet &called_type{to_code_type(called_function_sym.type)}; @@ -1706,7 +1706,7 @@ exprt statement_list_typecheckt::typecheck_function_call_arguments( for(const auto &assignment : assignments) { const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())}; - if(param_name == lhs.get_identifier()) + if(param_name == lhs.identifier()) { exprt assigned_variable{ typecheck_function_call_argument_rhs(tia_element, assignment.rhs())}; @@ -1736,7 +1736,7 @@ exprt statement_list_typecheckt::typecheck_function_call_argument_rhs( expr_try_dynamic_cast(rhs); if(symbol_rhs) assigned_operand = - typecheck_identifier(tia_element, symbol_rhs->get_identifier()); + typecheck_identifier(tia_element, symbol_rhs->identifier()); else // constant_exprt. assigned_operand = rhs; return assigned_operand; @@ -1750,11 +1750,11 @@ exprt statement_list_typecheckt::typecheck_return_value_assignment( for(const auto &assignment : assignments) { const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())}; - if(ID_statement_list_return_value_id == lhs.get_identifier()) + if(ID_statement_list_return_value_id == lhs.identifier()) { const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())}; const exprt assigned_variable{ - typecheck_identifier(tia_element, rhs.get_identifier())}; + typecheck_identifier(tia_element, rhs.identifier())}; if(return_type == assigned_variable.type()) return assigned_variable; else diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp index 9517d7299f7..f02aaf3fa2d 100644 --- a/src/util/find_macros.cpp +++ b/src/util/find_macros.cpp @@ -31,7 +31,7 @@ void find_macros( if(e.id() == ID_symbol) { - const irep_idt &identifier = to_symbol_expr(e).get_identifier(); + const irep_idt &identifier = to_symbol_expr(e).identifier(); const symbolt &symbol = ns.lookup(identifier); diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 488bad7e07f..4b15498c771 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -51,7 +51,7 @@ static bool find_symbols( const auto &binding_expr = to_binding_expr(src); std::unordered_set new_bindings{bindings}; for(const auto &v : binding_expr.variables()) - new_bindings.insert(v.get_identifier()); + new_bindings.insert(v.identifier()); if(!find_symbols( kind, binding_expr.where(), op, new_bindings, subs_to_find)) @@ -65,7 +65,7 @@ static bool find_symbols( const auto &let_expr = to_let_expr(src); std::unordered_set new_bindings{bindings}; for(const auto &v : let_expr.variables()) - new_bindings.insert(v.get_identifier()); + new_bindings.insert(v.identifier()); if(!find_symbols(kind, let_expr.where(), op, new_bindings, subs_to_find)) return false; @@ -112,7 +112,7 @@ static bool find_symbols( } else if(kind == symbol_kindt::F_EXPR_FREE) { - if(bindings.find(s.get_identifier()) == bindings.end() && !op(s)) + if(bindings.find(s.identifier()) == bindings.end() && !op(s)) return false; } } @@ -272,25 +272,32 @@ bool has_symbol_expr( return !find_symbols( include_bound_symbols ? symbol_kindt::F_EXPR : symbol_kindt::F_EXPR_FREE, src, - [&identifier](const symbol_exprt &e) { - return e.get_identifier() != identifier; - }); + [&identifier](const symbol_exprt &e) + { return e.identifier() != identifier; }); } void find_type_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); - return true; - }); + find_symbols( + symbol_kindt::F_TYPE, + src, + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); + return true; + }); } void find_type_symbols(const typet &src, find_symbols_sett &dest) { - find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); - return true; - }); + find_symbols( + symbol_kindt::F_TYPE, + src, + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); + return true; + }); } void find_non_pointer_type_symbols( @@ -298,8 +305,11 @@ void find_non_pointer_type_symbols( find_symbols_sett &dest) { find_symbols( - symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); + symbol_kindt::F_TYPE_NON_PTR, + src, + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); return true; }); } @@ -309,8 +319,11 @@ void find_non_pointer_type_symbols( find_symbols_sett &dest) { find_symbols( - symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); + symbol_kindt::F_TYPE_NON_PTR, + src, + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); return true; }); } @@ -323,8 +336,9 @@ void find_type_and_expr_symbols( find_symbols( symbol_kindt::F_ALL, src, - [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); return true; }, subs_to_find); @@ -338,8 +352,9 @@ void find_type_and_expr_symbols( find_symbols( symbol_kindt::F_ALL, src, - [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); return true; }, subs_to_find); @@ -347,8 +362,12 @@ void find_type_and_expr_symbols( void find_symbols(const exprt &src, find_symbols_sett &dest) { - find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) { - dest.insert(e.get_identifier()); - return true; - }); + find_symbols( + symbol_kindt::F_EXPR, + src, + [&dest](const symbol_exprt &e) + { + dest.insert(e.identifier()); + return true; + }); } diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 3cd1be097b7..2cb02f4950b 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -427,9 +427,8 @@ void format_expr_configt::setup() }; expr_map[ID_symbol] = - [](std::ostream &os, const exprt &expr) -> std::ostream & { - return os << to_symbol_expr(expr).get_identifier(); - }; + [](std::ostream &os, const exprt &expr) -> std::ostream & + { return os << to_symbol_expr(expr).identifier(); }; expr_map[ID_index] = [](std::ostream &os, const exprt &expr) -> std::ostream & { diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index da963951e7c..82c80725071 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -29,7 +29,7 @@ namespace_baset::~namespace_baset() /// INVARIANT. const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const { - return lookup(expr.get_identifier()); + return lookup(expr.identifier()); } /// Generic lookup function for a tag type in a symbol table. diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp index 8a118496546..7de79c38a1c 100644 --- a/src/util/pointer_expr.cpp +++ b/src/util/pointer_expr.cpp @@ -138,7 +138,7 @@ object_address_exprt::object_address_exprt( pointer_typet type) : nullary_exprt(ID_object_address, std::move(type)) { - set(ID_identifier, object.get_identifier()); + set(ID_identifier, object.identifier()); } symbol_exprt object_address_exprt::object_expr() const diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp index 3fe57c59bf3..9727ae1d336 100644 --- a/src/util/rename_symbol.cpp +++ b/src/util/rename_symbol.cpp @@ -23,7 +23,7 @@ void rename_symbolt::insert( const symbol_exprt &old_expr, const symbol_exprt &new_expr) { - insert_expr(old_expr.get_identifier(), new_expr.get_identifier()); + insert_expr(old_expr.identifier(), new_expr.identifier()); } bool rename_symbolt::rename(exprt &dest) const @@ -45,13 +45,13 @@ bool rename_symbolt::rename(exprt &dest) const if(it->id()==ID_symbol) { expr_mapt::const_iterator entry = - expr_map.find(to_symbol_expr(*it).get_identifier()); + expr_map.find(to_symbol_expr(*it).identifier()); if(entry != expr_map.end()) { if(!modifiable_expr) modifiable_expr = &it.mutate(); - to_symbol_expr(*modifiable_expr).set_identifier(entry->second); + to_symbol_expr(*modifiable_expr).identifier(entry->second); result = false; } } @@ -94,7 +94,7 @@ bool rename_symbolt::have_to_rename(const exprt &dest) const if(dest.id()==ID_symbol) { - const irep_idt &identifier = to_symbol_expr(dest).get_identifier(); + const irep_idt &identifier = to_symbol_expr(dest).identifier(); return expr_map.find(identifier) != expr_map.end(); } diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 7487f69c3bb..29dd2fe185a 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -29,20 +29,19 @@ void replace_symbolt::insert( old_expr.type() == new_expr.type(), "types to be replaced should match. old type:\n" + old_expr.type().pretty() + "\nnew.type:\n" + new_expr.type().pretty()); - expr_map.insert(std::pair( - old_expr.get_identifier(), new_expr)); + expr_map.insert(std::pair(old_expr.identifier(), new_expr)); } void replace_symbolt::set(const symbol_exprt &old_expr, const exprt &new_expr) { PRECONDITION(old_expr.type() == new_expr.type()); - expr_map[old_expr.get_identifier()] = new_expr; + expr_map[old_expr.identifier()] = new_expr; } bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const { - expr_mapt::const_iterator it = expr_map.find(s.get_identifier()); + expr_mapt::const_iterator it = expr_map.find(s.identifier()); if(it == expr_map.end()) return true; @@ -118,7 +117,7 @@ bool replace_symbolt::replace(exprt &dest) const // now set up the binding auto old_bindings = bindings; for(auto &variable : let_expr.variables()) - bindings.insert(variable.get_identifier()); + bindings.insert(variable.identifier()); // now replace in the 'where' expression if(!replace(let_expr.where())) @@ -134,7 +133,7 @@ bool replace_symbolt::replace(exprt &dest) const auto old_bindings = bindings; for(auto &binding : binding_expr.variables()) - bindings.insert(binding.get_identifier()); + bindings.insert(binding.identifier()); if(!replace(binding_expr.where())) result = false; @@ -175,7 +174,7 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const if(dest.id()==ID_symbol) { - const irep_idt &identifier = to_symbol_expr(dest).get_identifier(); + const irep_idt &identifier = to_symbol_expr(dest).identifier(); if(bindings.find(identifier) != bindings.end()) return false; else @@ -329,12 +328,12 @@ void unchecked_replace_symbolt::insert( const symbol_exprt &old_expr, const exprt &new_expr) { - expr_map.emplace(old_expr.get_identifier(), new_expr); + expr_map.emplace(old_expr.identifier(), new_expr); } bool unchecked_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const { - expr_mapt::const_iterator it = expr_map.find(s.get_identifier()); + expr_mapt::const_iterator it = expr_map.find(s.identifier()); if(it == expr_map.end()) return true; diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 8670a17b974..119e934854f 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -709,7 +709,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( if(expr.function().id() != ID_symbol) return unchanged(expr); - const irep_idt &func_id = to_symbol_expr(expr.function()).get_identifier(); + const irep_idt &func_id = to_symbol_expr(expr.function()).identifier(); // String.startsWith() is used to implement String.equals() in the models // library diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index d1afed4af5a..e9817ff0965 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -448,8 +448,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of( if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol) { - bool equal = to_symbol_expr(tmp0_object).get_identifier() == - to_symbol_expr(tmp1_object).get_identifier(); + bool equal = to_symbol_expr(tmp0_object).identifier() == + to_symbol_expr(tmp1_object).identifier(); return make_boolean_expr(expr.id() == ID_equal ? equal : !equal); } @@ -581,7 +581,7 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr) if(op_object.id() == ID_symbol) { - const irep_idt identifier = to_symbol_expr(op_object).get_identifier(); + const irep_idt identifier = to_symbol_expr(op_object).identifier(); // this is for the benefit of symex return make_boolean_expr( diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 624d43e3f22..ce2b5f8f4a3 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -514,7 +514,7 @@ try_get_string_data_array(const exprt &content, const namespacet &ns) const symbolt *symbol_ptr = nullptr; if( - ns.lookup(array.get_identifier(), symbol_ptr) || + ns.lookup(array.identifier(), symbol_ptr) || symbol_ptr->value.id() != ID_array) { return {}; diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index e92c79967e6..2edb9ef296a 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -32,7 +32,7 @@ initialize_ssa_identifier(std::ostream &os, const exprt &expr) return initialize_ssa_identifier(os, index->array()) << "[[" << idx << "]]"; } if(auto symbol = expr_try_dynamic_cast(expr)) - return os << symbol->get_identifier(); + return os << symbol->identifier(); UNREACHABLE; } @@ -45,7 +45,7 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type()) std::ostringstream os; initialize_ssa_identifier(os, expr); const std::string id = os.str(); - set_identifier(id); + identifier(id); set(ID_L1_object_identifier, id); } @@ -82,7 +82,7 @@ static void build_ssa_identifier_rec( } else if(expr.id()==ID_symbol) { - auto symid=to_symbol_expr(expr).get_identifier(); + auto symid = to_symbol_expr(expr).identifier(); os << symid; l1_object_os << symid; @@ -131,7 +131,7 @@ static void update_identifier(ssa_exprt &ssa) const irep_idt &l2 = ssa.get_level_2(); auto idpair = build_identifier(ssa.get_original_expr(), l0, l1, l2); - ssa.set_identifier(idpair.first); + ssa.identifier(idpair.first); ssa.set(ID_L1_object_identifier, idpair.second); } @@ -147,10 +147,10 @@ irep_idt ssa_exprt::get_object_name() const const exprt &original_expr = get_original_expr(); if(original_expr.id() == ID_symbol) - return to_symbol_expr(original_expr).get_identifier(); + return to_symbol_expr(original_expr).identifier(); return to_symbol_expr(object_descriptor_exprt::root_object(original_expr)) - .get_identifier(); + .identifier(); } const ssa_exprt ssa_exprt::get_l1_object() const @@ -199,7 +199,7 @@ void ssa_exprt::set_level_2(std::size_t i) void ssa_exprt::remove_level_2() { remove(ID_L2); - set_identifier(get_l1_object_identifier()); + identifier(get_l1_object_identifier()); } /* Used to determine whether or not an identifier can be built diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index c8a53e35d5a..87622ec2685 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -49,7 +49,7 @@ class ssa_exprt:public symbol_exprt const irep_idt get_original_name() const { ssa_exprt o(get_original_expr()); - return o.get_identifier(); + return o.identifier(); } void set_level_0(std::size_t i); diff --git a/src/util/std_code.h b/src/util/std_code.h index 6cd7f9eddd3..41f137b3dcf 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -363,7 +363,7 @@ class code_frontend_declt : public codet const irep_idt &get_identifier() const { - return symbol().get_identifier(); + return symbol().identifier(); } /// Returns the initial value to which the declared variable is initialized, @@ -411,7 +411,7 @@ class code_frontend_declt : public codet vm, code.op0().id() == ID_symbol, "declaring a non-symbol: " + - id2string(to_symbol_expr(code.op0()).get_identifier())); + id2string(to_symbol_expr(code.op0()).identifier())); } }; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 0623328d59e..fe99bb30a0e 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -435,7 +435,7 @@ exprt binding_exprt::instantiate(const operandst &values) const std::map substitutions; for(std::size_t i = 0; i < variables.size(); i++) - substitutions[variables[i].get_identifier()] = values[i]; + substitutions[variables[i].identifier()] = values[i]; // now recurse downwards and substitute in 'where' auto substitute_result = substitute_symbols(substitutions, where()); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 041f98385eb..5f20561db8b 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -131,33 +131,43 @@ class symbol_exprt : public nullary_exprt { public: /// \param type: Type of symbol - explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type)) + explicit symbol_exprt(typet type) : nullary_exprt{ID_symbol, std::move(type)} { } /// \param identifier: Name of symbol /// \param type: Type of symbol symbol_exprt(const irep_idt &identifier, typet type) - : nullary_exprt(ID_symbol, std::move(type)) + : nullary_exprt{ID_symbol, std::move(type)} { - set_identifier(identifier); + this->identifier(identifier); } /// Generate a symbol_exprt without a proper type. Use if, and only if, the - /// type either cannot be determined just yet (such as during type checking) - /// or when the type truly is immaterial. The latter case may better be dealt - /// with by using just an irep_idt, and not a symbol_exprt. + /// type either cannot be determined just yet (such as before type checking). static symbol_exprt typeless(const irep_idt &id) { - return symbol_exprt(id, typet()); + return symbol_exprt{id, typet{}}; } + DEPRECATED(SINCE(2026, 1, 18, "use identifier(...) instead")) void set_identifier(const irep_idt &identifier) + { + this->identifier(identifier); + } + + void identifier(const irep_idt &identifier) { set(ID_identifier, identifier); } + DEPRECATED(SINCE(2026, 1, 18, "use identifier() instead")) const irep_idt &get_identifier() const + { + return identifier(); + } + + const irep_idt &identifier() const { return get(ID_identifier); } @@ -204,7 +214,7 @@ struct hash<::symbol_exprt> { size_t operator()(const ::symbol_exprt &sym) { - return irep_id_hash()(sym.get_identifier()); + return irep_id_hash()(sym.identifier()); } }; } // namespace std diff --git a/src/util/substitute_symbols.cpp b/src/util/substitute_symbols.cpp index 95a2fc7ed76..d06574ebf0f 100644 --- a/src/util/substitute_symbols.cpp +++ b/src/util/substitute_symbols.cpp @@ -19,7 +19,7 @@ static std::optional substitute_symbols_rec( { if(src.id() == ID_symbol) { - auto s_it = substitutions.find(to_symbol_expr(src).get_identifier()); + auto s_it = substitutions.find(to_symbol_expr(src).identifier()); if(s_it == substitutions.end()) return {}; else @@ -34,7 +34,7 @@ static std::optional substitute_symbols_rec( // which may hide some of our substitutions auto new_substitutions = substitutions; for(const auto &variable : binding_expr.variables()) - new_substitutions.erase(variable.get_identifier()); + new_substitutions.erase(variable.identifier()); auto op_result = substitute_symbols_rec(new_substitutions, binding_expr.where()); @@ -56,7 +56,7 @@ static std::optional substitute_symbols_rec( // which may hide some of our substitutions auto new_substitutions = substitutions; for(const auto &variable : binding_expr.variables()) - new_substitutions.erase(variable.get_identifier()); + new_substitutions.erase(variable.identifier()); bool op_changed = false; diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp index 94160148a76..aa888cc33f3 100644 --- a/unit/analyses/ai/ai.cpp +++ b/unit/analyses/ai/ai.cpp @@ -89,8 +89,8 @@ class instruction_counter_analysist : public ait if(!i.is_assign()) return false; return i.assign_lhs().id() == ID_symbol && - id2string(to_symbol_expr(i.assign_lhs()).get_identifier()) - .find('y') != std::string::npos; + id2string(to_symbol_expr(i.assign_lhs()).identifier()).find('y') != + std::string::npos; } static bool is_y_assignment_location(locationt l) diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index b6961b99a0f..f8d57dca3cb 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -20,7 +20,7 @@ static bool starts_with_x(const exprt &e, const namespacet &) { if(e.id() != ID_symbol) return false; - return has_prefix(id2string(to_symbol_expr(e).get_identifier()), "x"); + return has_prefix(id2string(to_symbol_expr(e).identifier()), "x"); } SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") diff --git a/unit/analyses/variable-sensitivity/last_written_location.cpp b/unit/analyses/variable-sensitivity/last_written_location.cpp index 431493f2bef..542ab74f28f 100644 --- a/unit/analyses/variable-sensitivity/last_written_location.cpp +++ b/unit/analyses/variable-sensitivity/last_written_location.cpp @@ -36,14 +36,14 @@ SCENARIO( const irep_idt identifier = "hello"; auto first_val = symbol_exprt(identifier, integer_typet()); symbolt first_sym; - first_sym.name = first_val.get_identifier(); + first_sym.name = first_val.identifier(); auto rhs_val = from_integer(5, integer_typet()); const irep_idt second_identifier = "world"; auto second_val = symbol_exprt(second_identifier, integer_typet()); symbolt second_sym; - second_sym.name = second_val.get_identifier(); + second_sym.name = second_val.identifier(); symbol_tablet symbol_table; @@ -82,14 +82,14 @@ SCENARIO( const irep_idt identifier = "hello"; auto first_val = symbol_exprt(identifier, integer_typet()); symbolt first_sym; - first_sym.name = first_val.get_identifier(); + first_sym.name = first_val.identifier(); auto rhs_val = from_integer(5, integer_typet()); const irep_idt second_identifier = "world"; auto second_val = symbol_exprt(second_identifier, integer_typet()); symbolt second_sym; - second_sym.name = second_val.get_identifier(); + second_sym.name = second_val.identifier(); symbol_tablet symbol_table; diff --git a/unit/goto-programs/goto_program_goto_program_inline.cpp b/unit/goto-programs/goto_program_goto_program_inline.cpp index 06d1e475723..5463facad8e 100644 --- a/unit/goto-programs/goto_program_goto_program_inline.cpp +++ b/unit/goto-programs/goto_program_goto_program_inline.cpp @@ -54,11 +54,11 @@ TEST_CASE("Goto program inline", "[core][goto-programs][goto_program_inline]") const auto &lhs = it->assign_lhs(); if(assign_count == 0) { - REQUIRE(to_symbol_expr(lhs).get_identifier() == "x"); + REQUIRE(to_symbol_expr(lhs).identifier() == "x"); } else if(assign_count == 1) { - REQUIRE(to_symbol_expr(lhs).get_identifier() == "y"); + REQUIRE(to_symbol_expr(lhs).identifier() == "y"); } assign_count++; } diff --git a/unit/goto-programs/label_function_pointer_call_sites.cpp b/unit/goto-programs/label_function_pointer_call_sites.cpp index 8a3c345fea6..8eaa5ff413a 100644 --- a/unit/goto-programs/label_function_pointer_call_sites.cpp +++ b/unit/goto-programs/label_function_pointer_call_sites.cpp @@ -53,7 +53,7 @@ TEST_CASE("Label function pointer call sites", "[core]") // second call instruction const auto &fp_symbol = to_symbol_expr(to_dereference_expr(it->call_function()).pointer()) - .get_identifier(); + .identifier(); REQUIRE(fp_symbol == "h.function_pointer_call.1"); break; } @@ -62,7 +62,7 @@ TEST_CASE("Label function pointer call sites", "[core]") // third call instruction const auto &fp_symbol = to_symbol_expr(to_dereference_expr(it->call_function()).pointer()) - .get_identifier(); + .identifier(); REQUIRE(fp_symbol == "h.function_pointer_call.2"); auto it_prev = std::prev(it); @@ -71,7 +71,7 @@ TEST_CASE("Label function pointer call sites", "[core]") const auto &rhs = it_prev->assign_rhs(); REQUIRE( - to_symbol_expr(lhs).get_identifier() == "h.function_pointer_call.2"); + to_symbol_expr(lhs).identifier() == "h.function_pointer_call.2"); REQUIRE(rhs.id() == ID_if); diff --git a/unit/goto-programs/remove_returns.cpp b/unit/goto-programs/remove_returns.cpp index a56b5a4d701..b96fd15adde 100644 --- a/unit/goto-programs/remove_returns.cpp +++ b/unit/goto-programs/remove_returns.cpp @@ -30,7 +30,7 @@ TEST_CASE("Return-value removal", "[core][goto-programs][remove_returns]") symbol_exprt a_rv_symbol = return_value_symbol("a", ns); REQUIRE(is_return_value_symbol(a_rv_symbol)); - REQUIRE(is_return_value_identifier(a_rv_symbol.get_identifier())); + REQUIRE(is_return_value_identifier(a_rv_symbol.identifier())); irep_idt a_rv_id = return_value_identifier("a"); @@ -38,7 +38,7 @@ TEST_CASE("Return-value removal", "[core][goto-programs][remove_returns]") symbol_exprt other_symbol("a::local", signedbv_typet(8)); REQUIRE(!is_return_value_symbol(other_symbol)); - REQUIRE(!is_return_value_identifier(other_symbol.get_identifier())); + REQUIRE(!is_return_value_identifier(other_symbol.identifier())); } TEST_CASE( diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp index d207762c0a4..9702a683c53 100644 --- a/unit/goto-symex/apply_condition.cpp +++ b/unit/goto-symex/apply_condition.cpp @@ -17,7 +17,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; + symbolt symbol{symbol_expr.identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 9042248686e..e84340e6709 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -20,7 +20,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; + symbolt symbol{symbol_expr.identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); @@ -69,13 +69,13 @@ SCENARIO( state.assignment(ssa_foo, rhs1, ns, true, true, false); THEN("The result is `foo` renamed to L2") { - REQUIRE(result.get().get_identifier() == "foo!0#1"); + REQUIRE(result.get().identifier() == "foo!0#1"); } THEN("The propagation map contains an entry for `foo`") { const auto l1_foo = state.rename_ssa(ssa_foo, ns); const auto foo_propagated = - state.propagation.find(l1_foo.get().get_identifier()); + state.propagation.find(l1_foo.get().identifier()); REQUIRE(foo_propagated.has_value()); const auto foo_value = numeric_cast_v(to_constant_expr(foo_propagated->get())); @@ -93,13 +93,13 @@ SCENARIO( THEN("The level 2 index of `foo` is incremented") { - REQUIRE(result2.get().get_identifier() == "foo!0#2"); + REQUIRE(result2.get().identifier() == "foo!0#2"); } THEN("The propagation map entry for `foo` is updated") { const auto l1_foo = state.rename_ssa(ssa_foo, ns); const auto foo_propagated = - state.propagation.find(l1_foo.get().get_identifier()); + state.propagation.find(l1_foo.get().identifier()); REQUIRE(foo_propagated.has_value()); const auto foo_value = numeric_cast_v(to_constant_expr(foo_propagated->get())); @@ -131,7 +131,7 @@ SCENARIO( state.assignment(ssa_foo, null_pointer, ns, true, true, false); THEN("The result is `foo` renamed to L2") { - REQUIRE(result.get().get_identifier() == "foo!0#1"); + REQUIRE(result.get().identifier() == "foo!0#1"); } THEN("The value set contains an entry for `foo`") { @@ -159,7 +159,7 @@ SCENARIO( THEN("The level 2 index of `foo` is incremented") { - REQUIRE(result2.get().get_identifier() == "foo!0#2"); + REQUIRE(result2.get().identifier() == "foo!0#2"); } THEN("The value set for `foo` is updated to contain int_value!0") { @@ -172,7 +172,7 @@ SCENARIO( REQUIRE(object_descriptor != nullptr); const symbol_exprt object_symbol = to_symbol_expr(object_descriptor->object()); - REQUIRE(object_symbol.get_identifier() == "int_value!0"); + REQUIRE(object_symbol.identifier() == "int_value!0"); REQUIRE(object_descriptor->offset() == 0); } THEN("The target equations are unchanged") diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index 3464c3ba7c2..934138fe490 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -27,7 +27,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; + symbolt symbol{symbol_expr.identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); @@ -104,29 +104,27 @@ SCENARIO( THEN("The left-hand-side of the equation is foo!0#1") { - REQUIRE(to_symbol_expr(step.ssa_lhs).get_identifier() == "foo!0#1"); + REQUIRE(to_symbol_expr(step.ssa_lhs).identifier() == "foo!0#1"); } THEN("The right-hand-side of the equation is g!0#0 ? 475 : foo!0#0") { const if_exprt *rhs_if = expr_try_dynamic_cast(step.ssa_rhs); REQUIRE(rhs_if != nullptr); - REQUIRE(to_symbol_expr(rhs_if->cond()).get_identifier() == "g!0#0"); + REQUIRE(to_symbol_expr(rhs_if->cond()).identifier() == "g!0#0"); const auto then_value = numeric_cast_v(to_constant_expr(rhs_if->true_case())); REQUIRE(then_value == 475); const symbol_exprt rhs_symbol = to_symbol_expr(rhs_if->false_case()); - REQUIRE(rhs_symbol.get_identifier() == "foo!0#0"); + REQUIRE(rhs_symbol.identifier() == "foo!0#0"); } THEN("ssa_full_lhs is foo!0#1") { - REQUIRE( - to_symbol_expr(step.ssa_full_lhs).get_identifier() == "foo!0#1"); + REQUIRE(to_symbol_expr(step.ssa_full_lhs).identifier() == "foo!0#1"); } THEN("original_full_lhs is foo") { - REQUIRE( - to_symbol_expr(step.original_full_lhs).get_identifier() == "foo"); + REQUIRE(to_symbol_expr(step.original_full_lhs).identifier() == "foo"); } } } @@ -179,8 +177,7 @@ SCENARIO( THEN("The left-hand-side of the equation is foo!0#2") { - REQUIRE( - to_symbol_expr(step.ssa_lhs).get_identifier() == "foo!0#2"); + REQUIRE(to_symbol_expr(step.ssa_lhs).identifier() == "foo!0#2"); } THEN("The right-hand-side of the equation is 1841") { @@ -191,14 +188,12 @@ SCENARIO( THEN("ssa_full_lhs is foo!0#1") { REQUIRE( - to_symbol_expr(step.ssa_full_lhs).get_identifier() == - "foo!0#2"); + to_symbol_expr(step.ssa_full_lhs).identifier() == "foo!0#2"); } THEN("original_full_lhs is foo") { REQUIRE( - to_symbol_expr(step.original_full_lhs).get_identifier() == - "foo"); + to_symbol_expr(step.original_full_lhs).identifier() == "foo"); } } } @@ -244,7 +239,7 @@ SCENARIO( SSA_stept expand_step = target_equation.SSA_steps.back(); THEN("Assign step LHS is `struct1!0#1`") { - REQUIRE(assign_step.ssa_lhs.get_identifier() == "struct1!0#1"); + REQUIRE(assign_step.ssa_lhs.identifier() == "struct1!0#1"); } THEN("Assign step original full LHS is `struct1.field1`") { @@ -257,7 +252,7 @@ SCENARIO( const auto as_symbol = expr_try_dynamic_cast(assign_step.ssa_lhs); REQUIRE(as_symbol); - REQUIRE(as_symbol->get_identifier() == "struct1!0#1"); + REQUIRE(as_symbol->identifier() == "struct1!0#1"); } THEN("Assign step RHS is { struct1!0#0..field1 } with field1 = 234") { @@ -272,8 +267,7 @@ SCENARIO( } THEN("Expand step LHS is `struct1!0#2..field1`") { - REQUIRE( - expand_step.ssa_lhs.get_identifier() == "struct1!0#2..field1"); + REQUIRE(expand_step.ssa_lhs.identifier() == "struct1!0#2..field1"); } THEN("Expand step original full LHS is `struct1.field1`") { @@ -286,7 +280,7 @@ SCENARIO( const auto as_symbol = expr_try_dynamic_cast(expand_step.ssa_lhs); REQUIRE(as_symbol); - REQUIRE(as_symbol->get_identifier() == "struct1!0#2..field1"); + REQUIRE(as_symbol->identifier() == "struct1!0#2..field1"); } THEN("Expand step RHS is 234") { diff --git a/unit/goto-symex/symex_level0.cpp b/unit/goto-symex/symex_level0.cpp index b60e50eaad5..7759998307e 100644 --- a/unit/goto-symex/symex_level0.cpp +++ b/unit/goto-symex/symex_level0.cpp @@ -27,45 +27,53 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") const symbol_exprt symbol_nonshared{"nonShared", int_type}; const ssa_exprt ssa_nonshared{symbol_nonshared}; - symbol_table.insert([&] { - symbolt symbol{ - symbol_nonshared.get_identifier(), symbol_nonshared.type(), irep_idt{}}; - symbol.value = symbol_nonshared; - symbol.is_thread_local = true; - return symbol; - }()); + symbol_table.insert( + [&] + { + symbolt symbol{ + symbol_nonshared.identifier(), symbol_nonshared.type(), irep_idt{}}; + symbol.value = symbol_nonshared; + symbol.is_thread_local = true; + return symbol; + }()); const symbol_exprt symbol_shared{"shared", int_type}; const ssa_exprt ssa_shared{symbol_shared}; - symbol_table.insert([&] { - symbolt symbol{ - symbol_shared.get_identifier(), symbol_shared.type(), irep_idt{}}; - symbol.value = symbol_shared; - symbol.is_thread_local = false; - return symbol; - }()); + symbol_table.insert( + [&] + { + symbolt symbol{ + symbol_shared.identifier(), symbol_shared.type(), irep_idt{}}; + symbol.value = symbol_shared; + symbol.is_thread_local = false; + return symbol; + }()); const symbol_exprt symbol_guard{goto_symex_statet::guard_identifier(), bool_typet{}}; const ssa_exprt ssa_guard{symbol_guard}; - symbol_table.insert([&] { - symbolt symbol{ - symbol_guard.get_identifier(), symbol_guard.type(), irep_idt{}}; - symbol.value = symbol_guard; - symbol.is_thread_local = false; - return symbol; - }()); + symbol_table.insert( + [&] + { + symbolt symbol{ + symbol_guard.identifier(), symbol_guard.type(), irep_idt{}}; + symbol.value = symbol_guard; + symbol.is_thread_local = false; + return symbol; + }()); const code_typet code_type({}, int_type); const symbol_exprt symbol_fun{"fun", code_type}; const ssa_exprt ssa_fun{symbol_fun}; - symbol_table.insert([&] { - symbolt fun_symbol{ - symbol_fun.get_identifier(), symbol_fun.type(), irep_idt{}}; - fun_symbol.value = symbol_fun; - fun_symbol.is_thread_local = true; - return fun_symbol; - }()); + symbol_table.insert( + [&] + { + symbolt fun_symbol{ + symbol_fun.identifier(), symbol_fun.type(), irep_idt{}}; + fun_symbol.value = symbol_fun; + fun_symbol.is_thread_local = true; + return fun_symbol; + }()); WHEN("The non-shared symbol is renamed") { @@ -73,7 +81,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") THEN("Its L0 tag is set to the thread index") { - REQUIRE(renamed.get().get_identifier() == "nonShared!423"); + REQUIRE(renamed.get().identifier() == "nonShared!423"); } } @@ -83,7 +91,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") THEN("Its L0 tag is unchanged") { - REQUIRE(renamed.get().get_identifier() == "shared"); + REQUIRE(renamed.get().identifier() == "shared"); } } @@ -94,8 +102,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") THEN("Its L0 tag is unchanged") { REQUIRE( - renamed.get().get_identifier() == - goto_symex_statet::guard_identifier()); + renamed.get().identifier() == goto_symex_statet::guard_identifier()); } } @@ -105,7 +112,7 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") THEN("Its L0 tag is unchanged") { - REQUIRE(renamed.get().get_identifier() == "fun"); + REQUIRE(renamed.get().identifier() == "fun"); } } } diff --git a/unit/goto-symex/symex_level1.cpp b/unit/goto-symex/symex_level1.cpp index 27a783ba537..c949881ef1f 100644 --- a/unit/goto-symex/symex_level1.cpp +++ b/unit/goto-symex/symex_level1.cpp @@ -24,13 +24,15 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") const signedbv_typet int_type{32}; const symbol_exprt symbol_nonshared{"foo", int_type}; ssa_exprt ssa{symbol_nonshared}; - symbol_table.insert([&] { - symbolt symbol{ - symbol_nonshared.get_identifier(), symbol_nonshared.type(), irep_idt{}}; - symbol.value = symbol_nonshared; - symbol.is_thread_local = true; - return symbol; - }()); + symbol_table.insert( + [&] + { + symbolt symbol{ + symbol_nonshared.identifier(), symbol_nonshared.type(), irep_idt{}}; + symbol.value = symbol_nonshared; + symbol.is_thread_local = true; + return symbol; + }()); auto l0_symbol = symex_level0(ssa, ns, 50); symex_level1t symex_level1; @@ -40,7 +42,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") { REQUIRE(!symex_level1.has(l0_symbol)); auto renamed = symex_level1(l0_symbol); - REQUIRE(renamed.get().get_identifier() == "foo!50"); + REQUIRE(renamed.get().identifier() == "foo!50"); } } @@ -51,7 +53,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") { REQUIRE(symex_level1.has(l0_symbol)); auto renamed = symex_level1(l0_symbol); - REQUIRE(renamed.get().get_identifier() == "foo!50@12134"); + REQUIRE(renamed.get().identifier() == "foo!50@12134"); } auto old = symex_level1.insert_or_replace(l0_symbol, 43950); @@ -63,7 +65,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") THEN("The symbol is renamed to the new value") { auto renamed2 = symex_level1(l0_symbol); - REQUIRE(renamed2.get().get_identifier() == "foo!50@43950"); + REQUIRE(renamed2.get().identifier() == "foo!50@43950"); } REQUIRE(symex_level1.has(l0_symbol)); } @@ -79,7 +81,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") { REQUIRE(symex_level1.has(l0_symbol)); auto renamed = symex_level1(l0_symbol); - REQUIRE(renamed.get().get_identifier() == "foo!50@20051"); + REQUIRE(renamed.get().identifier() == "foo!50@20051"); } } } diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index b3ae467deba..f2dff4a284d 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -22,7 +22,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; + symbolt symbol{symbol_expr.identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 4a70592f67c..ec94f96b9ea 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1765,7 +1765,7 @@ TEST_CASE( test.object_size_function.make_application, test.is_dynamic_object_function.make_application); const smt_termt expected = smt_core_theoryt::equal( - smt_identifier_termt(symbol.get_identifier(), smt_bit_vector_sortt{64}), + smt_identifier_termt(symbol.identifier(), smt_bit_vector_sortt{64}), smt_bit_vector_theoryt::add( smt_bit_vector_theoryt::concat( smt_bit_vector_constant_termt{2, 8}, diff --git a/unit/testing-utils/require_expr.cpp b/unit/testing-utils/require_expr.cpp index 62ce8d59fac..f5fc7d32dc8 100644 --- a/unit/testing-utils/require_expr.cpp +++ b/unit/testing-utils/require_expr.cpp @@ -70,7 +70,7 @@ symbol_exprt require_expr::require_symbol( const exprt &expr, const irep_idt &symbol_name) { const symbol_exprt &symbol_expr = require_symbol(expr); - REQUIRE(symbol_expr.get_identifier()==symbol_name); + REQUIRE(symbol_expr.identifier() == symbol_name); return symbol_expr; } diff --git a/unit/util/ssa_expr.cpp b/unit/util/ssa_expr.cpp index 467fb711047..b9ba8ab4007 100644 --- a/unit/util/ssa_expr.cpp +++ b/unit/util/ssa_expr.cpp @@ -30,7 +30,7 @@ TEST_CASE("Constructor of ssa_exprt", "[unit][util][ssa_expr]") const ssa_exprt ssa{index}; THEN("the ssa_exprt has identifier 'sym..array_field[[9]]'") { - REQUIRE(ssa.get_identifier() == "sym..array_field[[9]]"); + REQUIRE(ssa.identifier() == "sym..array_field[[9]]"); REQUIRE(ssa.get_l1_object_identifier() == "sym..array_field[[9]]"); } THEN("the ssa_exprt has no level set") @@ -58,7 +58,7 @@ TEST_CASE("Set level", "[unit][util][ssa_expr]") REQUIRE(ssa.get_level_1() == irep_idt{}); REQUIRE(ssa.get_level_2() == irep_idt{}); REQUIRE(ssa.get_original_expr() == symbol); - REQUIRE(ssa.get_identifier() == "sym!1"); + REQUIRE(ssa.identifier() == "sym!1"); REQUIRE(ssa.get_l1_object_identifier() == "sym!1"); } @@ -69,7 +69,7 @@ TEST_CASE("Set level", "[unit][util][ssa_expr]") REQUIRE(ssa.get_level_1() == "3"); REQUIRE(ssa.get_level_2() == irep_idt{}); REQUIRE(ssa.get_original_expr() == symbol); - REQUIRE(ssa.get_identifier() == "sym@3"); + REQUIRE(ssa.identifier() == "sym@3"); REQUIRE(ssa.get_l1_object_identifier() == "sym@3"); } @@ -80,7 +80,7 @@ TEST_CASE("Set level", "[unit][util][ssa_expr]") REQUIRE(ssa.get_level_1() == irep_idt{}); REQUIRE(ssa.get_level_2() == "7"); REQUIRE(ssa.get_original_expr() == symbol); - REQUIRE(ssa.get_identifier() == "sym#7"); + REQUIRE(ssa.identifier() == "sym#7"); REQUIRE(ssa.get_l1_object_identifier() == "sym"); } } @@ -114,7 +114,7 @@ TEST_CASE("Set expression", "[unit][util][ssa_expr]") } THEN("The identifiers are updated") { - REQUIRE(ssa.get_identifier() == "sym!1@3#7[[9]]"); + REQUIRE(ssa.identifier() == "sym!1@3#7[[9]]"); REQUIRE(ssa.get_l1_object_identifier() == "sym!1@3[[9]]"); } } @@ -168,7 +168,7 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]") ssa.set_level_2(7); // Check we have constructed the desired SSA expression - REQUIRE(ssa.get_identifier() == "sym!1@3#7"); + REQUIRE(ssa.identifier() == "sym!1@3#7"); WHEN("get_l1_object is called on the SSA expression") { @@ -178,7 +178,7 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]") REQUIRE(l1_object.get_level_0() == "1"); REQUIRE(l1_object.get_level_1() == "3"); REQUIRE(l1_object.get_level_2() == irep_idt{}); - REQUIRE(l1_object.get_identifier() == "sym!1@3"); + REQUIRE(l1_object.identifier() == "sym!1@3"); } } } @@ -197,7 +197,7 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]") ssa.set_level_2(7); // Check we have constructed the desired SSA expression - REQUIRE(ssa.get_identifier() == "sym!1@3#7..array_field[[9]]"); + REQUIRE(ssa.identifier() == "sym!1@3#7..array_field[[9]]"); WHEN("get_l1_object is called on the SSA expression") { @@ -207,7 +207,7 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]") REQUIRE(l1_object.get_level_0() == "1"); REQUIRE(l1_object.get_level_1() == "3"); REQUIRE(l1_object.get_level_2() == irep_idt{}); - REQUIRE(l1_object.get_identifier() == "sym!1@3"); + REQUIRE(l1_object.identifier() == "sym!1@3"); } } }