diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 57a28f3a151..357a352da4e 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -358,17 +358,16 @@ void remove_exceptionst::add_exception_dispatch_sequence( stack_catch[i][j].second; if(!stack_catch[i][j].first.empty()) { - // Normal exception handler, make an instanceof check. - goto_programt::targett t_exc = goto_program.insert_after( - instr_it, - goto_programt::make_goto( - new_state_pc, true_exprt(), instr_it->source_location())); - // use instanceof to check that this is the correct handler struct_tag_typet type(stack_catch[i][j].first); java_instanceof_exprt check(exc_thrown, type); - t_exc->condition_nonconst() = check; + + // Normal exception handler, make an instanceof check. + goto_programt::targett t_exc = goto_program.insert_after( + instr_it, + goto_programt::make_goto( + new_state_pc, check, instr_it->source_location())); if(remove_added_instanceof) { diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index ab66e64cd6a..05377e0c167 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -294,10 +294,7 @@ static goto_programt::targett check_and_replace_target( inserted_expr.set_nullable( instr_info.get_nullable_type() == nondet_instruction_infot::is_nullablet::TRUE); - target_instruction->code_nonconst() = - code_assignt(nondet_var, inserted_expr); - target_instruction->code_nonconst().add_source_location() = - target_instruction->source_location(); + target_instruction->assign_rhs_nonconst() = inserted_expr; } goto_program.update(); diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index 1b62b796314..f9cc3cf1906 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -77,9 +77,9 @@ void instrument_intervals( { goto_programt::targett t=i_it; goto_function.body.insert_before_swap(i_it); - *t = goto_programt::make_assumption(conjunction(assertion)); i_it++; // goes to original instruction - t->source_location_nonconst() = i_it->source_location(); + *t = goto_programt::make_assumption( + conjunction(assertion), i_it->source_location()); } } } diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 8afe96ab0a6..355ffa36c19 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1724,20 +1724,25 @@ void goto_check_ct::add_guarded_property( if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second) { - auto t = new_code.add( - enable_assert_to_assume ? goto_programt::make_assumption( - std::move(guarded_expr), source_location) - : goto_programt::make_assertion( - std::move(guarded_expr), source_location)); - std::string source_expr_string; get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns); - t->source_location_nonconst().set_comment( - comment + " in " + source_expr_string); - t->source_location_nonconst().set_property_class(property_class); + source_locationt annotated_location = source_location; + annotated_location.set_comment(comment + " in " + source_expr_string); + annotated_location.set_property_class(property_class); + + add_all_disable_named_check_pragmas(annotated_location); - add_all_disable_named_check_pragmas(t->source_location_nonconst()); + if(enable_assert_to_assume) + { + new_code.add(goto_programt::make_assumption( + std::move(guarded_expr), annotated_location)); + } + else + { + new_code.add(goto_programt::make_assertion( + std::move(guarded_expr), annotated_location)); + } } } @@ -2120,15 +2125,21 @@ void goto_check_ct::goto_check( { if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end()) { - auto t = new_code.add( - enable_assert_to_assume - ? goto_programt::make_assumption(false_exprt{}, i.source_location()) - : goto_programt::make_assertion( - false_exprt{}, i.source_location())); - - t->source_location_nonconst().set_property_class("error label"); - t->source_location_nonconst().set_comment("error label " + label); - t->source_location_nonconst().set("user-provided", true); + source_locationt annotated_location = i.source_location(); + annotated_location.set_property_class("error label"); + annotated_location.set_comment("error label " + label); + annotated_location.set("user-provided", true); + + if(enable_assert_to_assume) + { + new_code.add( + goto_programt::make_assumption(false_exprt{}, annotated_location)); + } + else + { + new_code.add( + goto_programt::make_assertion(false_exprt{}, annotated_location)); + } } } @@ -2210,10 +2221,9 @@ void goto_check_ct::goto_check( side_effect_expr_nondett(bool_typet(), i.source_location()), std::move(address_of_expr), lhs); - goto_programt::targett t = - new_code.add(goto_programt::make_assignment( - std::move(lhs), std::move(rhs), i.source_location())); - t->code_nonconst().add_source_location() = i.source_location(); + new_code.add(goto_programt::make_assignment( + code_assignt{std::move(lhs), std::move(rhs), i.source_location()}, + i.source_location())); } } } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index f47a93dc54c..f09c2f8891e 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -179,12 +179,13 @@ void taint_analysist::instrument( where, ID_get_may, address_of_exprt(string_constantt(rule.taint))}; - goto_programt::targett t = - insert_before.add(goto_programt::make_assertion( - not_exprt(get_may), instruction.source_location())); - t->source_location_nonconst().set_property_class( + source_locationt annotated_location = + instruction.source_location(); + annotated_location.set_property_class( "taint rule " + id2string(rule.id)); - t->source_location_nonconst().set_comment(rule.message); + annotated_location.set_comment(rule.message); + insert_before.add(goto_programt::make_assertion( + not_exprt(get_may), annotated_location)); break; } diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index 00a958a4df7..fe55bfc5c27 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -164,8 +164,8 @@ void memory_snapshot_harness_generatort::add_init_section( auto ins_it1 = goto_program.insert_before( start_it, - goto_programt::make_goto(goto_program.const_cast_target(start_it))); - ins_it1->condition_nonconst() = func_init_done_var; + goto_programt::make_goto( + goto_program.const_cast_target(start_it), func_init_done_var)); auto ins_it2 = goto_program.insert_after( ins_it1, diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp index f69ce37bbc2..4598b91698a 100644 --- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp +++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp @@ -52,15 +52,13 @@ void overflow_instrumentert::add_overflow_checks( if(t->is_assign()) { - code_assignt &assignment = to_code_assign(t->code_nonconst()); - - if(assignment.lhs()==overflow_var) + if(t->assign_lhs() == overflow_var) { return; } - add_overflow_checks(t, assignment.lhs(), added); - add_overflow_checks(t, assignment.rhs(), added); + add_overflow_checks(t, t->assign_lhs_nonconst(), added); + add_overflow_checks(t, t->assign_rhs_nonconst(), added); } if(t->has_condition()) diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index eb739bf4a50..8af85dff76b 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -145,12 +145,10 @@ void scratch_programt::fix_types() { if(it->is_assign()) { - code_assignt &code = to_code_assign(it->code_nonconst()); - - if(code.lhs().type()!=code.rhs().type()) + if(it->assign_lhs().type() != it->assign_rhs().type()) { - typecast_exprt typecast(code.rhs(), code.lhs().type()); - code.rhs()=typecast; + typecast_exprt typecast{it->assign_rhs(), it->assign_lhs().type()}; + it->assign_rhs_nonconst() = typecast; } } else if(it->is_assume() || it->is_assert()) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 530a48c6a67..3b29d0f1c36 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -278,10 +278,9 @@ void code_contractst::check_apply_loop_contracts( { code_assertt assertion{initial_invariant_val}; assertion.add_source_location() = loop_head_location; + assertion.add_source_location().set_comment( + "Check loop invariant before entry"); converter.goto_convert(assertion, pre_loop_head_instrs, mode); - pre_loop_head_instrs.instructions.back() - .source_location_nonconst() - .set_comment("Check loop invariant before entry"); } // Insert the first block of pre_loop_head_instrs, @@ -396,10 +395,9 @@ void code_contractst::check_apply_loop_contracts( { code_assertt assertion{invariant}; assertion.add_source_location() = loop_head_location; + assertion.add_source_location().set_comment( + "Check that loop invariant is preserved"); converter.goto_convert(assertion, pre_loop_end_instrs, mode); - pre_loop_end_instrs.instructions.back() - .source_location_nonconst() - .set_comment("Check that loop invariant is preserved"); } // Generate: assignments to store the multidimensional decreases clause's @@ -421,11 +419,10 @@ void code_contractst::check_apply_loop_contracts( generate_lexicographic_less_than_check( new_decreases_vars, old_decreases_vars)}; monotonic_decreasing_assertion.add_source_location() = loop_head_location; + monotonic_decreasing_assertion.add_source_location().set_comment( + "Check decreases clause on loop iteration"); converter.goto_convert( monotonic_decreasing_assertion, pre_loop_end_instrs, mode); - pre_loop_end_instrs.instructions.back() - .source_location_nonconst() - .set_comment("Check decreases clause on loop iteration"); // Discard the temporary variables that store decreases clause's value for(size_t i = 0; i < old_decreases_vars.size(); i++) @@ -464,12 +461,12 @@ void code_contractst::check_apply_loop_contracts( goto_programt pre_loop_exit_instrs; // Assertion to check that step case was checked if we entered the loop. + source_locationt annotated_location = loop_head_location; + annotated_location.set_comment( + "Check that loop instrumentation was not truncated"); pre_loop_exit_instrs.add(goto_programt::make_assertion( or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}}, - loop_head_location)); - pre_loop_exit_instrs.instructions.back() - .source_location_nonconst() - .set_comment("Check that loop instrumentation was not truncated"); + annotated_location)); // Instructions to make all the temporaries go dead. pre_loop_exit_instrs.add( goto_programt::make_dead(in_base_case, loop_head_location)); @@ -873,9 +870,8 @@ void code_contractst::apply_function_contract( goto_programt::make_decl(to_symbol_expr(call_ret), loc)); side_effect_expr_nondett expr(type, location); - auto target = havoc_instructions.add( - goto_programt::make_assignment(call_ret, expr, loc)); - target->code_nonconst().add_source_location() = loc; + havoc_instructions.add(goto_programt::make_assignment( + code_assignt{call_ret, std::move(expr), loc}, loc)); } // Insert havoc instructions immediately before the call site. diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index 81dff575e03..1404a6b728b 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -83,9 +83,9 @@ void havoc_assigns_clause_targetst::havoc_if_valid( { // OTHER __CPROVER_havoc_object(target_snapshot_var) codet code(ID_havoc_object, {car.lower_bound_var()}); - const auto &inst = - dest.add(goto_programt::make_other(code, source_location)); - inst->source_location_nonconst().set_comment(tracking_comment); + source_locationt annotated_location = source_location; + annotated_location.set_comment(tracking_comment); + dest.add(goto_programt::make_other(code, annotated_location)); } else if(car.havoc_method == car_havoc_methodt::HAVOC_SLICE) { @@ -106,12 +106,13 @@ void havoc_assigns_clause_targetst::havoc_if_valid( // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type()) const auto &target_type = car.target().type(); side_effect_expr_nondett nondet(target_type, source_location); - const auto &inst = dest.add(goto_programt::make_assignment( + source_locationt annotated_location = source_location; + annotated_location.set_comment(tracking_comment); + dest.add(goto_programt::make_assignment( dereference_exprt{typecast_exprt::conditional_cast( car.lower_bound_var(), pointer_type(target_type))}, nondet, - source_location)); - inst->source_location_nonconst().set_comment(tracking_comment); + annotated_location)); } else { @@ -154,10 +155,11 @@ void havoc_assigns_clause_targetst::havoc_static_local( const auto &target_type = car.target().type(); side_effect_expr_nondett nondet(target_type, source_location); - const auto &inst = dest.add( - goto_programt::make_assignment(car.target(), nondet, source_location)); - inst->source_location_nonconst().set_comment(tracking_comment); - add_propagate_static_local_pragma(inst->source_location_nonconst()); + source_locationt annotated_location = source_location; + annotated_location.set_comment(tracking_comment); + add_propagate_static_local_pragma(annotated_location); + dest.add( + goto_programt::make_assignment(car.target(), nondet, annotated_location)); dest.destructive_append(skip_program); diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h index 521022a357b..0f5bddecb2c 100644 --- a/src/goto-instrument/cover_instrument.h +++ b/src/goto-instrument/cover_instrument.h @@ -81,15 +81,14 @@ class cover_instrumenter_baset const assertion_factoryt &) const = 0; void initialize_source_location( - goto_programt::targett t, + source_locationt &source_location, const std::string &comment, const irep_idt &function_id) const { - t->source_location_nonconst().set_comment(comment); - t->source_location_nonconst().set( - ID_coverage_criterion, coverage_criterion); - t->source_location_nonconst().set_property_class(property_class); - t->source_location_nonconst().set_function(function_id); + source_location.set_comment(comment); + source_location.set(ID_coverage_criterion, coverage_criterion); + source_location.set_property_class(property_class); + source_location.set_function(function_id); } bool is_non_cover_assertion(goto_programt::const_targett t) const diff --git a/src/goto-instrument/cover_instrument_assume.cpp b/src/goto-instrument/cover_instrument_assume.cpp index bc3a728b11e..7714b45ec21 100644 --- a/src/goto-instrument/cover_instrument_assume.cpp +++ b/src/goto-instrument/cover_instrument_assume.cpp @@ -23,7 +23,6 @@ void cover_assume_instrumentert::instrument( { if(i_it->is_assume()) { - const auto location = i_it->source_location(); const auto assume_condition = expr2c(i_it->condition(), namespacet{symbol_tablet()}); const auto comment_before = @@ -31,13 +30,14 @@ void cover_assume_instrumentert::instrument( const auto comment_after = "assert(false) after assume(" + assume_condition + ")"; + source_locationt location = i_it->source_location(); + initialize_source_location(location, comment_before, function_id); const auto assert_before = make_assertion(false_exprt{}, location); - goto_programt::targett t = goto_program.insert_before(i_it, assert_before); - initialize_source_location(t, comment_before, function_id); + goto_program.insert_before(i_it, assert_before); + initialize_source_location(location, comment_after, function_id); const auto assert_after = make_assertion(false_exprt{}, location); - t = goto_program.insert_after(i_it, assert_after); - initialize_source_location(t, comment_after, function_id); + goto_program.insert_after(i_it, assert_after); } // Otherwise, skip existing assertions. else if(i_it->is_assert()) diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp index 99a3b20476c..efec9d5409c 100644 --- a/src/goto-instrument/cover_instrument_branch.cpp +++ b/src/goto-instrument/cover_instrument_branch.cpp @@ -40,10 +40,9 @@ void cover_branch_instrumentert::instrument( std::string comment = "entry point"; source_locationt source_location = i_it->source_location(); - - goto_programt::targett t = goto_program.insert_before( + initialize_source_location(source_location, comment, function_id); + goto_program.insert_before( i_it, make_assertion(false_exprt(), source_location)); - initialize_source_location(t, comment, function_id); } if(is_conditional_goto) @@ -57,12 +56,12 @@ void cover_branch_instrumentert::instrument( source_locationt source_location = i_it->source_location(); goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, true_comment, function_id); *i_it = make_assertion(not_exprt(guard), source_location); - initialize_source_location(i_it, true_comment, function_id); goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, false_comment, function_id); *i_it = make_assertion(guard, source_location); - initialize_source_location(i_it, false_comment, function_id); std::advance(i_it, 2); } diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp index 423df0d0bca..9e5c319db8f 100644 --- a/src/goto-instrument/cover_instrument_condition.cpp +++ b/src/goto-instrument/cover_instrument_condition.cpp @@ -30,7 +30,7 @@ void cover_condition_instrumentert::instrument( { const std::set conditions = collect_conditions(i_it); - const source_locationt source_location = i_it->source_location(); + source_locationt source_location = i_it->source_location(); for(const auto &c : conditions) { @@ -38,13 +38,13 @@ void cover_condition_instrumentert::instrument( const std::string comment_t = "condition '" + c_string + "' true"; goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, comment_t, function_id); *i_it = make_assertion(c, source_location); - initialize_source_location(i_it, comment_t, function_id); const std::string comment_f = "condition '" + c_string + "' false"; goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, comment_f, function_id); *i_it = make_assertion(not_exprt(c), source_location); - initialize_source_location(i_it, comment_f, function_id); } for(std::size_t i = 0; i < conditions.size() * 2; i++) diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp index d0b00bcc38f..adefbd528da 100644 --- a/src/goto-instrument/cover_instrument_decision.cpp +++ b/src/goto-instrument/cover_instrument_decision.cpp @@ -30,7 +30,7 @@ void cover_decision_instrumentert::instrument( { const std::set decisions = collect_decisions(i_it); - const source_locationt source_location = i_it->source_location(); + source_locationt source_location = i_it->source_location(); for(const auto &d : decisions) { @@ -38,13 +38,13 @@ void cover_decision_instrumentert::instrument( const std::string comment_t = "decision '" + d_string + "' true"; goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, comment_t, function_id); *i_it = make_assertion(d, source_location); - initialize_source_location(i_it, comment_t, function_id); const std::string comment_f = "decision '" + d_string + "' false"; goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, comment_f, function_id); *i_it = make_assertion(not_exprt(d), source_location); - initialize_source_location(i_it, comment_f, function_id); } // advance iterator beyond the inserted instructions diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp index 4de7e1dd651..64b93dc1936 100644 --- a/src/goto-instrument/cover_instrument_location.cpp +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -31,7 +31,8 @@ void cover_location_instrumentert::instrument( { const std::string b = std::to_string(block_nr + 1); // start with 1 const std::string id = id2string(function_id) + "#" + b; - auto source_location = basic_blocks.source_location_of(block_nr); + source_locationt source_location = + basic_blocks.source_location_of(block_nr); // filter goals if(goal_filters(source_location)) @@ -41,8 +42,8 @@ void cover_location_instrumentert::instrument( "block " + b + " (lines " + source_lines.to_string() + ")"; source_location.set_basic_block_source_lines(source_lines.to_irep()); goto_program.insert_before_swap(i_it); + initialize_source_location(source_location, comment, function_id); *i_it = make_assertion(false_exprt(), source_location); - initialize_source_location(i_it, comment, function_id); i_it++; } } diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index 52ac7599366..7656f6617d1 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -662,21 +662,21 @@ void cover_mcdc_instrumentert::instrument( std::string comment_t = description + " '" + p_string + "' true"; goto_program.insert_before_swap(i_it); - *i_it = make_assertion(not_exprt(p), source_location); - i_it->source_location_nonconst().set_comment(comment_t); - i_it->source_location_nonconst().set( - ID_coverage_criterion, coverage_criterion); - i_it->source_location_nonconst().set_property_class(property_class); - i_it->source_location_nonconst().set_function(function_id); + source_locationt annotated_location = source_location; + annotated_location.set_comment(comment_t); + annotated_location.set(ID_coverage_criterion, coverage_criterion); + annotated_location.set_property_class(property_class); + annotated_location.set_function(function_id); + *i_it = make_assertion(not_exprt(p), annotated_location); std::string comment_f = description + " '" + p_string + "' false"; goto_program.insert_before_swap(i_it); - *i_it = make_assertion(p, source_location); - i_it->source_location_nonconst().set_comment(comment_f); - i_it->source_location_nonconst().set( - ID_coverage_criterion, coverage_criterion); - i_it->source_location_nonconst().set_property_class(property_class); - i_it->source_location_nonconst().set_function(function_id); + annotated_location = source_location; + annotated_location.set_comment(comment_f); + annotated_location.set(ID_coverage_criterion, coverage_criterion); + annotated_location.set_property_class(property_class); + annotated_location.set_function(function_id); + *i_it = make_assertion(p, annotated_location); } std::set controlling; @@ -697,12 +697,12 @@ void cover_mcdc_instrumentert::instrument( "MC/DC independence condition '" + p_string + "'"; goto_program.insert_before_swap(i_it); - *i_it = make_assertion(not_exprt(p), source_location); - i_it->source_location_nonconst().set_comment(description); - i_it->source_location_nonconst().set( - ID_coverage_criterion, coverage_criterion); - i_it->source_location_nonconst().set_property_class(property_class); - i_it->source_location_nonconst().set_function(function_id); + source_locationt annotated_location = source_location; + annotated_location.set_comment(description); + annotated_location.set(ID_coverage_criterion, coverage_criterion); + annotated_location.set_property_class(property_class); + annotated_location.set_function(function_id); + *i_it = make_assertion(not_exprt(p), annotated_location); } for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++) diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index f870176daff..c86e3af073d 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -42,7 +42,9 @@ void cover_assertion_instrumentert::instrument( { i_it->condition_nonconst() = false_exprt(); initialize_source_location( - i_it, id2string(i_it->source_location().get_comment()), function_id); + i_it->source_location_nonconst(), + id2string(i_it->source_location().get_comment()), + function_id); } } @@ -65,7 +67,8 @@ void cover_cover_instrumentert::instrument( const exprt c = i_it->call_arguments()[0]; *i_it = make_assertion(not_exprt(c), i_it->source_location()); std::string comment = "condition '" + from_expr(ns, function_id, c) + "'"; - initialize_source_location(i_it, comment, function_id); + initialize_source_location( + i_it->source_location_nonconst(), comment, function_id); } } else if(is_non_cover_assertion(i_it)) @@ -94,9 +97,9 @@ void cover_instrument_end_of_function( const std::string &comment = "additional goal to ensure reachability of end of function"; goto_program.insert_before_swap(if_it); - *if_it = make_assertion(false_exprt(), location); - if_it->source_location_nonconst().set_comment(comment); - if_it->source_location_nonconst().set_property_class( - "reachability_constraint"); - if_it->source_location_nonconst().set_function(function_id); + source_locationt annotated_location = location; + annotated_location.set_comment(comment); + annotated_location.set_property_class("reachability_constraint"); + annotated_location.set_function(function_id); + *if_it = make_assertion(false_exprt(), annotated_location); } diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 0e05b3c4156..7a7b7e6a61f 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -76,14 +76,10 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); - // NOLINTNEXTLINE - auto add_instruction = [&](goto_programt::instructiont &&i) { - auto instruction = function.body.add(std::move(i)); - instruction->source_location_nonconst() = function_symbol.location; - return instruction; - }; - add_instruction(goto_programt::make_assumption(false_exprt())); - add_instruction(goto_programt::make_end_function()); + function.body.add( + goto_programt::make_assumption(false_exprt(), function_symbol.location)); + function.body.add( + goto_programt::make_end_function(function_symbol.location)); } }; @@ -96,20 +92,17 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); - // NOLINTNEXTLINE - auto add_instruction = [&](goto_programt::instructiont &&i) { - auto instruction = function.body.add(std::move(i)); - instruction->source_location_nonconst() = function_symbol.location; - instruction->source_location_nonconst().set_function(function_name); - return instruction; - }; - auto assert_instruction = - add_instruction(goto_programt::make_assertion(false_exprt())); - assert_instruction->source_location_nonconst().set_comment( - "undefined function should be unreachable"); - assert_instruction->source_location_nonconst().set_property_class( - ID_assertion); - add_instruction(goto_programt::make_end_function()); + + source_locationt annotated_location = function_symbol.location; + annotated_location.set_function(function_name); + annotated_location.set_comment("undefined function should be unreachable"); + annotated_location.set_property_class(ID_assertion); + function.body.add( + goto_programt::make_assertion(false_exprt(), annotated_location)); + + source_locationt location = function_symbol.location; + location.set_function(function_name); + function.body.add(goto_programt::make_end_function(location)); } }; @@ -123,21 +116,18 @@ class assert_false_then_assume_false_generate_function_bodiest const irep_idt &function_name) const override { auto const &function_symbol = symbol_table.lookup_ref(function_name); - // NOLINTNEXTLINE - auto add_instruction = [&](goto_programt::instructiont &&i) { - auto instruction = function.body.add(std::move(i)); - instruction->source_location_nonconst() = function_symbol.location; - instruction->source_location_nonconst().set_function(function_name); - return instruction; - }; - auto assert_instruction = - add_instruction(goto_programt::make_assertion(false_exprt())); - assert_instruction->source_location_nonconst().set_comment( - "undefined function should be unreachable"); - assert_instruction->source_location_nonconst().set_property_class( - ID_assertion); - add_instruction(goto_programt::make_assumption(false_exprt())); - add_instruction(goto_programt::make_end_function()); + + source_locationt annotated_location = function_symbol.location; + annotated_location.set_function(function_name); + annotated_location.set_comment("undefined function should be unreachable"); + annotated_location.set_property_class(ID_assertion); + function.body.add( + goto_programt::make_assertion(false_exprt(), annotated_location)); + + source_locationt location = function_symbol.location; + location.set_function(function_name); + function.body.add(goto_programt::make_assumption(false_exprt(), location)); + function.body.add(goto_programt::make_end_function(location)); } }; @@ -259,12 +249,6 @@ class havoc_generate_function_bodiest : public generate_function_bodiest } auto const &function_symbol = symbol_table.lookup_ref(function_name); - // NOLINTNEXTLINE - auto add_instruction = [&](goto_programt::instructiont &&i) { - auto instruction = function.body.add(std::move(i)); - instruction->source_location_nonconst() = function_symbol.location; - return instruction; - }; for(std::size_t i = 0; i < function.parameter_identifiers.size(); ++i) { @@ -278,9 +262,11 @@ class havoc_generate_function_bodiest : public generate_function_bodiest should_havoc_param(id2string(parameter_symbol.base_name), i)) { auto goto_instruction = - add_instruction(goto_programt::make_incomplete_goto(equal_exprt( - parameter_symbol.symbol_expr(), - null_pointer_exprt(to_pointer_type(parameter_symbol.type))))); + function.body.add(goto_programt::make_incomplete_goto( + equal_exprt( + parameter_symbol.symbol_expr(), + null_pointer_exprt(to_pointer_type(parameter_symbol.type))), + function_symbol.location)); dereference_exprt dereference_expr( parameter_symbol.symbol_expr(), @@ -297,7 +283,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest function.body.destructive_append(dest); - auto label_instruction = add_instruction(goto_programt::make_skip()); + auto label_instruction = + function.body.add(goto_programt::make_skip(function_symbol.location)); goto_instruction->complete_goto(label_instruction); } } @@ -335,7 +322,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest aux_symbol.is_static_lifetime = false; - add_instruction(goto_programt::make_decl(aux_symbol.symbol_expr())); + function.body.add(goto_programt::make_decl( + aux_symbol.symbol_expr(), function_symbol.location)); goto_programt dest; @@ -352,13 +340,15 @@ class havoc_generate_function_bodiest : public generate_function_bodiest exprt return_expr = typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type); - add_instruction( - goto_programt::make_set_return_value(std::move(return_expr))); + function.body.add(goto_programt::make_set_return_value( + std::move(return_expr), function_symbol.location)); - add_instruction(goto_programt::make_dead(aux_symbol.symbol_expr())); + function.body.add(goto_programt::make_dead( + aux_symbol.symbol_expr(), function_symbol.location)); } - add_instruction(goto_programt::make_end_function()); + function.body.add( + goto_programt::make_end_function(function_symbol.location)); remove_skip(function.body); } @@ -623,8 +613,7 @@ void generate_function_bodies( { if(instruction.is_function_call()) { - auto &called_function = - to_code_function_call(instruction.code_nonconst()).function(); + auto &called_function = instruction.call_function(); if(is_havoc_function_call(called_function)) { if(++counter == *call_site_number) diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp index 385d4942174..185b010140b 100644 --- a/src/goto-instrument/havoc_utils.cpp +++ b/src/goto-instrument/havoc_utils.cpp @@ -60,7 +60,6 @@ void havoc_utilst::append_scalar_havoc_code_for_expr( goto_programt &dest) const { side_effect_expr_nondett rhs(expr.type(), location); - goto_programt::targett t = - dest.add(goto_programt::make_assignment(expr, std::move(rhs), location)); - t->code_nonconst().add_source_location() = location; + dest.add(goto_programt::make_assignment( + code_assignt{expr, std::move(rhs), location}, location)); } diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 0ed287dadce..a08e8bdef10 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -198,20 +198,18 @@ static void race_check( if(!is_shared(ns, w_entry.second.symbol_expr)) continue; - goto_programt::targett t = goto_program.insert_before( + goto_program.insert_before( i_it, goto_programt::make_assignment( w_guards.get_w_guard_expr(w_entry.second), w_entry.second.guard, original_instruction.source_location())); - i_it=++t; } // insert original statement here { goto_programt::targett t=goto_program.insert_before(i_it); *t=original_instruction; - i_it=++t; } // now add assignments for what is written -- reset @@ -220,13 +218,12 @@ static void race_check( if(!is_shared(ns, w_entry.second.symbol_expr)) continue; - goto_programt::targett t = goto_program.insert_before( + goto_program.insert_before( i_it, goto_programt::make_assignment( w_guards.get_w_guard_expr(w_entry.second), false_exprt(), original_instruction.source_location())); - i_it = std::next(t); } // now add assertions for what is read and written @@ -235,14 +232,13 @@ static void race_check( if(!is_shared(ns, r_entry.second.symbol_expr)) continue; - goto_programt::targett t = goto_program.insert_before( + source_locationt annotated_location = + original_instruction.source_location(); + annotated_location.set_comment(comment(r_entry.second, false)); + goto_program.insert_before( i_it, goto_programt::make_assertion( - w_guards.get_assertion(r_entry.second), - original_instruction.source_location())); - t->source_location_nonconst().set_comment( - comment(r_entry.second, false)); - i_it=++t; + w_guards.get_assertion(r_entry.second), annotated_location)); } for(const auto &w_entry : rw_set.w_entries) @@ -250,14 +246,13 @@ static void race_check( if(!is_shared(ns, w_entry.second.symbol_expr)) continue; - goto_programt::targett t = goto_program.insert_before( + source_locationt annotated_location = + original_instruction.source_location(); + annotated_location.set_comment(comment(w_entry.second, true)); + goto_program.insert_before( i_it, goto_programt::make_assertion( - w_guards.get_assertion(w_entry.second), - original_instruction.source_location())); - t->source_location_nonconst().set_comment( - comment(w_entry.second, true)); - i_it=++t; + w_guards.get_assertion(w_entry.second), annotated_location)); } i_it--; // the for loop already counts us up diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 5a300f18761..a40a0eddf0e 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -69,12 +69,12 @@ static void stack_depth( goto_programt::targett first=goto_program.instructions.begin(); binary_relation_exprt guard(symbol, ID_le, max_depth); - goto_programt::targett assert_ins = goto_program.insert_before( - first, goto_programt::make_assertion(guard, first->source_location())); - - assert_ins->source_location_nonconst().set_comment( + source_locationt annotated_location = first->source_location(); + annotated_location.set_comment( "Stack depth exceeds " + std::to_string(i_depth)); - assert_ins->source_location_nonconst().set_property_class("stack-depth"); + annotated_location.set_property_class("stack-depth"); + goto_program.insert_before( + first, goto_programt::make_assertion(guard, annotated_location)); goto_program.insert_before( first, diff --git a/src/goto-instrument/synthesizer/synthesizer_utils.cpp b/src/goto-instrument/synthesizer/synthesizer_utils.cpp index 12fcd1e4284..f871fce7a6e 100644 --- a/src/goto-instrument/synthesizer/synthesizer_utils.cpp +++ b/src/goto-instrument/synthesizer/synthesizer_utils.cpp @@ -106,7 +106,6 @@ void annotate_invariants( goto_programt::targett loop_end = get_loop_end(loop_number, function); // annotate the invariant to the condition of `loop_end` - exprt condition = loop_end->condition(); loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) = invariant_map_entry.second; } diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp index 8b3debe3c5f..631ecee1b90 100644 --- a/src/goto-instrument/thread_instrumentation.cpp +++ b/src/goto-instrument/thread_instrumentation.cpp @@ -35,8 +35,6 @@ void thread_exit_instrumentation(goto_programt &goto_program) assert(end->is_end_function()); - source_locationt source_location = end->source_location(); - goto_program.insert_before_swap(end); const string_constantt mutex_locked_string("mutex-locked"); @@ -47,10 +45,9 @@ void thread_exit_instrumentation(goto_programt &goto_program) ID_get_may, address_of_exprt(mutex_locked_string)}; + source_locationt source_location = end->source_location(); + source_location.set_comment("mutexes must not be locked on thread exit"); *end = goto_programt::make_assertion(not_exprt(get_may), source_location); - - end->source_location_nonconst().set_comment( - "mutexes must not be locked on thread exit"); } void thread_exit_instrumentation(goto_modelt &goto_model) diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-instrument/undefined_functions.cpp index 510a8c62900..6a71afeebfe 100644 --- a/src/goto-instrument/undefined_functions.cpp +++ b/src/goto-instrument/undefined_functions.cpp @@ -58,10 +58,10 @@ void undefined_function_abort_path(goto_modelt &goto_model) if(entry->second.body_available()) continue; - ins = - goto_programt::make_assumption(false_exprt(), ins.source_location()); - ins.source_location_nonconst().set_comment( + source_locationt annotated_location = ins.source_location(); + annotated_location.set_comment( "'" + id2string(function_identifier) + "' is undefined"); + ins = goto_programt::make_assumption(false_exprt(), annotated_location); } } } diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index a80099b6d39..3860358ae7e 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -153,14 +153,13 @@ void uninitializedt::add_assertions( const irep_idt new_identifier=id2string(identifier)+"#initialized"; // insert assertion + source_locationt annotated_location = instruction.source_location(); + annotated_location.set_comment( + "use of uninitialized local variable " + id2string(identifier)); + annotated_location.set_property_class("uninitialized local"); goto_programt::instructiont assertion = goto_programt::make_assertion( - symbol_exprt(new_identifier, bool_typet()), - instruction.source_location()); - assertion.source_location_nonconst().set_comment( - "use of uninitialized local variable " + id2string(identifier)); - assertion.source_location_nonconst().set_property_class( - "uninitialized local"); + symbol_exprt(new_identifier, bool_typet()), annotated_location); goto_program.insert_before_swap(i_it, assertion); i_it++; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 3bb44a0ec4c..38f6567f41a 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -698,12 +698,12 @@ void goto_convertt::do_havoc_slice( r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]); ok_expr.add_source_location() = source_location; - goto_programt::targett t = - dest.add(goto_programt::make_assertion(ok_expr, source_location)); - t->source_location_nonconst().set("user-provided", false); - t->source_location_nonconst().set_property_class(ID_assertion); - t->source_location_nonconst().set_comment( + source_locationt annotated_location = source_location; + annotated_location.set("user-provided", false); + annotated_location.set_property_class(ID_assertion); + annotated_location.set_comment( "assertion havoc_slice " + from_expr(ns, identifier, ok_expr)); + dest.add(goto_programt::make_assertion(ok_expr, annotated_location)); const array_typet array_type(char_type(), simplify_expr(arguments[1], ns)); @@ -782,11 +782,11 @@ void goto_convertt::do_function_call_symbol( } // let's double-check the type of the argument - goto_programt::targett t = dest.add(goto_programt::make_assumption( + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + dest.add(goto_programt::make_assumption( typecast_exprt::conditional_cast(arguments.front(), bool_typet()), - function.source_location())); - - t->source_location_nonconst().set("user-provided", true); + annotated_location)); if(lhs.is_not_nil()) { @@ -804,11 +804,10 @@ void goto_convertt::do_function_call_symbol( throw 0; } - goto_programt::targett t = dest.add( - goto_programt::make_assertion(false_exprt(), function.source_location())); - - t->source_location_nonconst().set("user-provided", true); - t->source_location_nonconst().set_property_class(ID_assertion); + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + annotated_location.set_property_class(ID_assertion); + dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); if(lhs.is_not_nil()) { @@ -819,9 +818,9 @@ void goto_convertt::do_function_call_symbol( // __VERIFIER_error has abort() semantics, even if no assertions // are being checked - goto_programt::targett a = dest.add(goto_programt::make_assumption( - false_exprt(), function.source_location())); - a->source_location_nonconst().set("user-provided", true); + annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + dest.add(goto_programt::make_assumption(false_exprt(), annotated_location)); } else if( identifier == "assert" && @@ -835,13 +834,14 @@ void goto_convertt::do_function_call_symbol( } // let's double-check the type of the argument - goto_programt::targett t = dest.add(goto_programt::make_assertion( - typecast_exprt::conditional_cast(arguments.front(), bool_typet()), - function.source_location())); - t->source_location_nonconst().set("user-provided", true); - t->source_location_nonconst().set_property_class(ID_assertion); - t->source_location_nonconst().set_comment( + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + annotated_location.set_property_class(ID_assertion); + annotated_location.set_comment( "assertion " + from_expr(ns, identifier, arguments.front())); + dest.add(goto_programt::make_assertion( + typecast_exprt::conditional_cast(arguments.front(), bool_typet()), + annotated_location)); if(lhs.is_not_nil()) { @@ -874,26 +874,27 @@ void goto_convertt::do_function_call_symbol( get_string_constant(arguments[1]); // let's double-check the type of the argument - goto_programt::targett t = dest.add(goto_programt::make_assertion( - typecast_exprt::conditional_cast(arguments[0], bool_typet()), - function.source_location())); - + source_locationt annotated_location = function.source_location(); if(is_precondition) { - t->source_location_nonconst().set_property_class(ID_precondition); + annotated_location.set_property_class(ID_precondition); } else if(is_postcondition) { - t->source_location_nonconst().set_property_class(ID_postcondition); + annotated_location.set_property_class(ID_postcondition); } else { - t->source_location_nonconst().set( + annotated_location.set( "user-provided", !function.source_location().is_built_in()); - t->source_location_nonconst().set_property_class(ID_assertion); + annotated_location.set_property_class(ID_assertion); } - t->source_location_nonconst().set_comment(description); + annotated_location.set_comment(description); + + dest.add(goto_programt::make_assertion( + typecast_exprt::conditional_cast(arguments[0], bool_typet()), + annotated_location)); if(lhs.is_not_nil()) { @@ -1085,12 +1086,11 @@ void goto_convertt::do_function_call_symbol( const irep_idt description= "assertion "+id2string(get_string_constant(arguments[0])); - goto_programt::targett t = dest.add( - goto_programt::make_assertion(false_exprt(), function.source_location())); - - t->source_location_nonconst().set("user-provided", true); - t->source_location_nonconst().set_property_class(ID_assertion); - t->source_location_nonconst().set_comment(description); + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + annotated_location.set_property_class(ID_assertion); + annotated_location.set_comment(description); + dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } else if(identifier=="__assert_rtn" || @@ -1123,12 +1123,11 @@ void goto_convertt::do_function_call_symbol( throw 0; } - goto_programt::targett t = dest.add( - goto_programt::make_assertion(false_exprt(), function.source_location())); - - t->source_location_nonconst().set("user-provided", true); - t->source_location_nonconst().set_property_class(ID_assertion); - t->source_location_nonconst().set_comment(description); + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + annotated_location.set_property_class(ID_assertion); + annotated_location.set_comment(description); + dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } else if(identifier=="__assert_func") @@ -1157,12 +1156,11 @@ void goto_convertt::do_function_call_symbol( description="assertion"; } - goto_programt::targett t = dest.add( - goto_programt::make_assertion(false_exprt(), function.source_location())); - - t->source_location_nonconst().set("user-provided", true); - t->source_location_nonconst().set_property_class(ID_assertion); - t->source_location_nonconst().set_comment(description); + source_locationt annotated_location = function.source_location(); + annotated_location.set("user-provided", true); + annotated_location.set_property_class(ID_assertion); + annotated_location.set_comment(description); + dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } else if(identifier==CPROVER_PREFIX "fence") diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index f2ffb1df759..63e0d793971 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -833,9 +833,9 @@ void goto_convertt::convert_assert( clean_expr(cond, dest, mode); - goto_programt::targett t = - dest.add(goto_programt::make_assertion(cond, code.source_location())); - t->source_location_nonconst().set("user-provided", true); + source_locationt annotated_location = code.source_location(); + annotated_location.set("user-provided", true); + dest.add(goto_programt::make_assertion(cond, annotated_location)); } void goto_convertt::convert_skip( @@ -1606,8 +1606,8 @@ void goto_convertt::generate_ifthenelse( // do the x label goto_programt tmp_x; - goto_programt::targett x = - tmp_x.add(goto_programt::make_incomplete_goto(true_exprt())); + goto_programt::targett x = tmp_x.add(goto_programt::make_incomplete_goto( + true_exprt(), true_case.instructions.back().source_location())); // do the z label goto_programt tmp_z; @@ -1636,7 +1636,6 @@ void goto_convertt::generate_ifthenelse( // x: goto z; CHECK_RETURN(!tmp_w.instructions.empty()); x->complete_goto(z); - x->source_location_nonconst() = tmp_w.instructions.back().source_location(); dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); @@ -1957,13 +1956,12 @@ void goto_convertt::generate_thread_block( goto_programt::targett c = body.add(goto_programt::make_skip()); convert(thread_body, body, mode); - goto_programt::targett e = postamble.add(goto_programt::instructiont( + postamble.add(goto_programt::instructiont( static_cast(get_nil_irep()), thread_body.source_location(), END_THREAD, nil_exprt(), {})); - e->source_location_nonconst() = thread_body.source_location(); goto_programt::targett z = postamble.add(goto_programt::make_skip()); preamble.add(goto_programt::instructiont( diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 324b3e84594..6bec969876d 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -213,10 +213,8 @@ void goto_convert_functionst::convert_function( !f.body.instructions.empty() && has_prefix(id2string(identifier), "__VERIFIER_atomic_")) { - goto_programt::instructiont a_begin; - a_begin = goto_programt::make_atomic_begin(); - a_begin.source_location_nonconst() = - f.body.instructions.front().source_location(); + goto_programt::instructiont a_begin = goto_programt::make_atomic_begin( + f.body.instructions.front().source_location()); f.body.insert_before_swap(f.body.instructions.begin(), a_begin); goto_programt::targett a_end = diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index be6764834d4..f577aca2b49 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -47,9 +47,9 @@ void goto_inlinet::parameter_assignments( // this is the type the n-th argument should have const typet ¶meter_type = symbol.type; - goto_programt::targett decl = - dest.add(goto_programt::make_decl(symbol.symbol_expr(), source_location)); - decl->code_nonconst().add_source_location() = source_location; + code_declt decl{symbol.symbol_expr()}; + decl.add_source_location() = source_location; + dest.add(goto_programt::make_decl(std::move(decl), source_location)); // this is the actual parameter exprt actual; diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index 9cd2a07f3b8..0f1fd3cbd7a 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -129,11 +129,10 @@ void instrument_preconditions( goto_program.insert_before_swap(it); exprt instance = p->condition(); r(instance); - *it = goto_programt::make_assertion(instance, source_location); - it->source_location_nonconst().set_property_class( - ID_precondition_instance); - it->source_location_nonconst().set_comment( - p->source_location().get_comment()); + source_locationt annotated_location = source_location; + annotated_location.set_property_class(ID_precondition_instance); + annotated_location.set_comment(p->source_location().get_comment()); + *it = goto_programt::make_assertion(instance, annotated_location); it++; } } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 8ea768eba13..23c8b068ad0 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -238,7 +238,8 @@ static void fix_return_type( dest.add(goto_programt::make_assignment(code_assignt( old_lhs, make_byte_extract( - tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type())))); + tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()), + function_call.source_location()))); } void remove_function_pointerst::remove_function_pointer( @@ -388,7 +389,8 @@ void remove_function_pointer( // the final target is a skip goto_programt final_skip; - goto_programt::targett t_final = final_skip.add(goto_programt::make_skip()); + goto_programt::targett t_final = + final_skip.add(goto_programt::make_skip(target->source_location())); // build the calls and gotos @@ -407,11 +409,13 @@ void remove_function_pointer( goto_programt tmp; fix_return_type(function_id, new_call, symbol_table, tmp); - auto call = new_code_calls.add(goto_programt::make_function_call(new_call)); + auto call = new_code_calls.add( + goto_programt::make_function_call(new_call, target->source_location())); new_code_calls.destructive_append(tmp); // goto final - new_code_calls.add(goto_programt::make_goto(t_final, true_exprt())); + new_code_calls.add(goto_programt::make_goto( + t_final, true_exprt(), target->source_location())); // goto to call const address_of_exprt address_of(fun, pointer_type(fun.type())); @@ -419,17 +423,18 @@ void remove_function_pointer( const auto casted_address = typecast_exprt::conditional_cast(address_of, pointer.type()); - new_code_gotos.add( - goto_programt::make_goto(call, equal_exprt(pointer, casted_address))); + new_code_gotos.add(goto_programt::make_goto( + call, equal_exprt(pointer, casted_address), target->source_location())); } // fall-through - goto_programt::targett t = - new_code_gotos.add(goto_programt::make_assertion(false_exprt())); - t->source_location_nonconst().set_property_class("pointer dereference"); - t->source_location_nonconst().set_comment( - function_pointer_assertion_comment(functions)); - new_code_gotos.add(goto_programt::make_assumption(false_exprt())); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("pointer dereference"); + annotated_location.set_comment(function_pointer_assertion_comment(functions)); + new_code_gotos.add( + goto_programt::make_assertion(false_exprt(), annotated_location)); + new_code_gotos.add( + goto_programt::make_assumption(false_exprt(), target->source_location())); goto_programt new_code; @@ -438,20 +443,6 @@ void remove_function_pointer( new_code.destructive_append(new_code_calls); new_code.destructive_append(final_skip); - // set locations - for(auto &instruction : new_code.instructions) - { - source_locationt &source_location = instruction.source_location_nonconst(); - - irep_idt property_class = source_location.get_property_class(); - irep_idt comment = source_location.get_comment(); - source_location = target->source_location(); - if(!property_class.empty()) - source_location.set_property_class(property_class); - if(!comment.empty()) - source_location.set_comment(comment); - } - goto_programt::targett next_target=target; next_target++; diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 8e30fb8a890..d2addae6546 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -141,12 +141,15 @@ static void create_static_function_call( /// the virtual function call /// \param temp_var_for_this: The new expression for the this argument of the /// virtual function call +/// \param vcall_source_loc: The source location of the function call, which is +/// used for new instructions that are added /// \return A goto program consisting of all the amended asserts and assumes static goto_programt analyse_checks_directly_preceding_function_call( const goto_programt &goto_program, goto_programt::const_targett instr_it, const exprt &argument_for_this, - const symbol_exprt &temp_var_for_this) + const symbol_exprt &temp_var_for_this, + const source_locationt &vcall_source_loc) { goto_programt checks_directly_preceding_function_call; @@ -181,7 +184,7 @@ static goto_programt analyse_checks_directly_preceding_function_call( { checks_directly_preceding_function_call.insert_before( checks_directly_preceding_function_call.instructions.cbegin(), - goto_programt::make_assumption(guard)); + goto_programt::make_assumption(guard, vcall_source_loc)); } } @@ -230,7 +233,11 @@ static void process_this_argument( goto_programt checks_directly_preceding_function_call = analyse_checks_directly_preceding_function_call( - goto_program, target, argument_for_this, temp_var_for_this); + goto_program, + target, + argument_for_this, + temp_var_for_this, + vcall_source_loc); new_code_for_this_argument.destructive_append( checks_directly_preceding_function_call); @@ -377,16 +384,14 @@ static goto_programt::targett replace_virtual_function_with_dispatch_table( } else { - goto_programt::targett t1 = new_code_calls.add( - goto_programt::make_assertion(false_exprt(), vcall_source_loc)); - + source_locationt annotated_location = vcall_source_loc; // No definition for this type; shouldn't be possible... - t1->source_location_nonconst().set_comment( + annotated_location.set_comment( "cannot find calls for " + id2string(code.function().get(ID_identifier)) + " dispatching " + id2string(fun.class_id)); - - insertit.first->second = t1; + insertit.first->second = new_code_calls.add( + goto_programt::make_assertion(false_exprt(), annotated_location)); } // goto final @@ -441,20 +446,6 @@ static goto_programt::targett replace_virtual_function_with_dispatch_table( new_code.destructive_append(new_code_calls); new_code.destructive_append(final_skip); - // set locations - for(auto &instruction : new_code.instructions) - { - source_locationt &source_location = instruction.source_location_nonconst(); - - const irep_idt property_class = source_location.get_property_class(); - const irep_idt comment = source_location.get_comment(); - source_location = target->source_location(); - if(!property_class.empty()) - source_location.set_property_class(property_class); - if(!comment.empty()) - source_location.set_comment(comment); - } - goto_program.destructive_insert(next_target, new_code); // finally, kill original invocation diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 1f5acc0c285..4dd82ced8f6 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -306,10 +306,10 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest, { const symbolt &symbol=ns.lookup(identifier); symbol_exprt sym_expr=symbol.symbol_expr(); - - goto_programt::targett decl1 = - dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location())); - decl1->code_nonconst().add_source_location() = ref_instr->source_location(); + code_declt decl{sym_expr}; + decl.add_source_location() = ref_instr->source_location(); + dest.add( + goto_programt::make_decl(std::move(decl), ref_instr->source_location())); exprt val=symbol.value; // initialize pointers with suitable objects @@ -322,11 +322,9 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest, // may still be nil (structs, then assignments have been done already) if(val.is_not_nil()) { - goto_programt::targett assignment1 = - dest.add(goto_programt::make_assignment( - code_assignt(sym_expr, val), ref_instr->source_location())); - assignment1->code_nonconst().add_source_location() = - ref_instr->source_location(); + code_assignt assignment{sym_expr, val, ref_instr->source_location()}; + dest.add( + goto_programt::make_assignment(assignment, ref_instr->source_location())); } } @@ -384,11 +382,9 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest, member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type()); - goto_programt::targett assignment1 = - dest.add(goto_programt::make_assignment( - code_assignt(member, sym_expr), ref_instr->source_location())); - assignment1->code_nonconst().add_source_location() = - ref_instr->source_location(); + code_assignt assignment{member, sym_expr, ref_instr->source_location()}; + dest.add(goto_programt::make_assignment( + code_assignt(member, sym_expr), ref_instr->source_location())); } ++seen; @@ -431,9 +427,10 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( symbol_exprt sym_expr=new_symbol.symbol_expr(); // make sure it is declared before the recursive call - goto_programt::targett decl = - dest.add(goto_programt::make_decl(sym_expr, ref_instr->source_location())); - decl->code_nonconst().add_source_location() = ref_instr->source_location(); + code_declt decl{sym_expr}; + decl.add_source_location() = ref_instr->source_location(); + dest.add( + goto_programt::make_decl(std::move(decl), ref_instr->source_location())); // set the value - may be nil if( @@ -457,12 +454,10 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( if(new_symbol.value.is_not_nil()) { - goto_programt::targett assignment1 = - dest.add(goto_programt::make_assignment( - code_assignt(sym_expr, new_symbol.value), - ref_instr->source_location())); - assignment1->code_nonconst().add_source_location() = - ref_instr->source_location(); + code_assignt assignment{ + sym_expr, new_symbol.value, ref_instr->source_location()}; + dest.add( + goto_programt::make_assignment(assignment, ref_instr->source_location())); } goto_model.symbol_table.insert(std::move(new_symbol)); @@ -1071,8 +1066,12 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol, if(symbol.is_static_lifetime) { goto_programt::targett dummy_loc = - initialization.add(goto_programt::instructiont()); - dummy_loc->source_location_nonconst() = symbol.location; + initialization.add(goto_programt::instructiont{ + codet{ID_nil}, + symbol.location, + goto_program_instruction_typet::NO_INSTRUCTION_TYPE, + {}, + {}}); make_decl_and_def(initialization, dummy_loc, identifier, symbol.name); initialization.instructions.erase(dummy_loc); } @@ -1172,11 +1171,9 @@ goto_programt::targett string_abstractiont::abstract_pointer_assign( if(lhs.type().id()==ID_pointer && !unknown) { - goto_programt::instructiont assignment; - assignment = goto_programt::make_assignment( - code_assignt(new_lhs, new_rhs), target->source_location()); - assignment.code_nonconst().add_source_location() = - target->source_location(); + goto_programt::instructiont assignment = goto_programt::make_assignment( + code_assignt(new_lhs, new_rhs, target->source_location()), + target->source_location()); dest.insert_before_swap(target, assignment); return std::next(target); @@ -1264,18 +1261,14 @@ goto_programt::targett string_abstractiont::char_assign( i1.is_not_nil(), "failed to create is_zero-component for the left-hand-side"); - goto_programt::targett assignment1 = tmp.add(goto_programt::make_assignment( - code_assignt(i1, from_integer(1, i1.type())), target->source_location())); - assignment1->code_nonconst().add_source_location() = - target->source_location(); - - goto_programt::targett assignment2 = tmp.add(goto_programt::make_assignment( - code_assignt(lhs, rhs), target->source_location())); - assignment2->code_nonconst().add_source_location() = - target->source_location(); + tmp.add(goto_programt::make_assignment( + code_assignt(i1, from_integer(1, i1.type()), target->source_location()), + target->source_location())); - move_lhs_arithmetic( - assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1()); + code_assignt assignment{lhs, rhs, target->source_location()}; + move_lhs_arithmetic(assignment.lhs(), assignment.rhs()); + tmp.add( + goto_programt::make_assignment(assignment, target->source_location())); dest.insert_before_swap(target, tmp); ++target; @@ -1370,32 +1363,26 @@ goto_programt::targett string_abstractiont::value_assignments_string_struct( // copy all the values goto_programt tmp; - { - goto_programt::targett assignment = tmp.add(goto_programt::make_assignment( + tmp.add(goto_programt::make_assignment( + code_assignt{ member(lhs, whatt::IS_ZERO), member(rhs, whatt::IS_ZERO), - target->source_location())); - assignment->code_nonconst().add_source_location() = - target->source_location(); - } + target->source_location()}, + target->source_location())); - { - goto_programt::targett assignment = tmp.add(goto_programt::make_assignment( + tmp.add(goto_programt::make_assignment( + code_assignt{ member(lhs, whatt::LENGTH), member(rhs, whatt::LENGTH), - target->source_location())); - assignment->code_nonconst().add_source_location() = - target->source_location(); - } + target->source_location()}, + target->source_location())); - { - goto_programt::targett assignment = tmp.add(goto_programt::make_assignment( + tmp.add(goto_programt::make_assignment( + code_assignt{ member(lhs, whatt::SIZE), member(rhs, whatt::SIZE), - target->source_location())); - assignment->code_nonconst().add_source_location() = - target->source_location(); - } + target->source_location()}, + target->source_location())); goto_programt::targett last=target; ++last; diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index cd17afd6848..2c5424e6b61 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -275,10 +275,10 @@ void string_instrumentationt::do_sprintf( // in the abstract model, we have to report a // (possibly false) positive here - goto_programt::targett assertion = tmp.add( - goto_programt::make_assertion(false_exprt(), target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); - assertion->source_location_nonconst().set_comment("sprintf buffer overflow"); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment("sprintf buffer overflow"); + tmp.add(goto_programt::make_assertion(false_exprt(), annotated_location)); do_format_string_read(tmp, target, arguments, 1, 2, "sprintf"); @@ -311,11 +311,11 @@ void string_instrumentationt::do_snprintf( exprt bufsize = buffer_size(arguments[0]); - goto_programt::targett assertion = tmp.add(goto_programt::make_assertion( - binary_relation_exprt(bufsize, ID_ge, arguments[1]), - target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); - assertion->source_location_nonconst().set_comment("snprintf buffer overflow"); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment("snprintf buffer overflow"); + tmp.add(goto_programt::make_assertion( + binary_relation_exprt(bufsize, ID_ge, arguments[1]), annotated_location)); do_format_string_read(tmp, target, arguments, 2, 3, "snprintf"); @@ -399,13 +399,13 @@ void string_instrumentationt::do_format_string_read( temp=address_of_exprt(index); } - goto_programt::targett assertion = - dest.add(goto_programt::make_assertion( - is_zero_string(temp), target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); std::string comment("zero-termination of string argument of "); comment += function_name; - assertion->source_location_nonconst().set_comment(comment); + annotated_location.set_comment(comment); + dest.add(goto_programt::make_assertion( + is_zero_string(temp), annotated_location)); } } @@ -422,11 +422,12 @@ void string_instrumentationt::do_format_string_read( } else // non-const format string { - goto_programt::targett format_ass = dest.add(goto_programt::make_assertion( - is_zero_string(arguments[1]), target->source_location())); - format_ass->source_location_nonconst().set_property_class("string"); - format_ass->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of format string of " + function_name); + dest.add(goto_programt::make_assertion( + is_zero_string(arguments[1]), annotated_location)); for(std::size_t i=2; isource_location())); - assertion->source_location_nonconst().set_property_class("string"); - assertion->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of string argument of " + function_name); + dest.add(goto_programt::make_assertion( + is_zero_string(temp), annotated_location)); } } } @@ -521,13 +522,13 @@ void string_instrumentationt::do_format_string_write( condition = false_exprt(); } - goto_programt::targett assertion = - dest.add(goto_programt::make_assertion( - condition, target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); std::string comment("format string buffer overflow in "); comment += function_name; - assertion->source_location_nonconst().set_comment(comment); + annotated_location.set_comment(comment); + dest.add( + goto_programt::make_assertion(condition, annotated_location)); // now kill the contents invalidate_buffer( @@ -576,13 +577,13 @@ void string_instrumentationt::do_format_string_write( // as we don't know any field width for the %s that // should be here during runtime, we just report a // possibly false positive - goto_programt::targett assertion = - dest.add(goto_programt::make_assertion( - false_exprt(), target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); std::string comment("format string buffer overflow in "); comment += function_name; - assertion->source_location_nonconst().set_comment(comment); + annotated_location.set_comment(comment); + dest.add( + goto_programt::make_assertion(false_exprt(), annotated_location)); invalidate_buffer(dest, target, arguments[i], arg_type, 0); } @@ -619,16 +620,15 @@ void string_instrumentationt::do_strchr( "strchr expected to have two arguments", target->source_location()); } - goto_programt tmp; - - goto_programt::targett assertion = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[0]), target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); - assertion->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of string argument of strchr"); + goto_programt::instructiont assertion = goto_programt::make_assertion( + is_zero_string(arguments[0]), annotated_location); target->turn_into_skip(); - dest.insert_before_swap(target, tmp); + dest.insert_before_swap(target, assertion); } void string_instrumentationt::do_strrchr( @@ -643,16 +643,15 @@ void string_instrumentationt::do_strrchr( "strrchr expected to have two arguments", target->source_location()); } - goto_programt tmp; - - goto_programt::targett assertion = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[0]), target->source_location())); - assertion->source_location_nonconst().set_property_class("string"); - assertion->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of string argument of strrchr"); + goto_programt::instructiont assertion = goto_programt::make_assertion( + is_zero_string(arguments[0]), annotated_location); target->turn_into_skip(); - dest.insert_before_swap(target, tmp); + dest.insert_before_swap(target, assertion); } void string_instrumentationt::do_strstr( @@ -669,17 +668,18 @@ void string_instrumentationt::do_strstr( goto_programt tmp; - goto_programt::targett assertion0 = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[0]), target->source_location())); - assertion0->source_location_nonconst().set_property_class("string"); - assertion0->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of 1st string argument of strstr"); + tmp.add(goto_programt::make_assertion( + is_zero_string(arguments[0]), annotated_location)); - goto_programt::targett assertion1 = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[1]), target->source_location())); - assertion1->source_location_nonconst().set_property_class("string"); - assertion1->source_location_nonconst().set_comment( + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of 2nd string argument of strstr"); + tmp.add(goto_programt::make_assertion( + is_zero_string(arguments[1]), annotated_location)); target->turn_into_skip(); dest.insert_before_swap(target, tmp); @@ -699,17 +699,18 @@ void string_instrumentationt::do_strtok( goto_programt tmp; - goto_programt::targett assertion0 = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[0]), target->source_location())); - assertion0->source_location_nonconst().set_property_class("string"); - assertion0->source_location_nonconst().set_comment( + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of 1st string argument of strtok"); + tmp.add(goto_programt::make_assertion( + is_zero_string(arguments[0]), annotated_location)); - goto_programt::targett assertion1 = tmp.add(goto_programt::make_assertion( - is_zero_string(arguments[1]), target->source_location())); - assertion1->source_location_nonconst().set_property_class("string"); - assertion1->source_location_nonconst().set_comment( + annotated_location.set_property_class("string"); + annotated_location.set_comment( "zero-termination of 2nd string argument of strtok"); + tmp.add(goto_programt::make_assertion( + is_zero_string(arguments[1]), annotated_location)); target->turn_into_skip(); dest.insert_before_swap(target, tmp); @@ -860,12 +861,16 @@ void string_instrumentationt::invalidate_buffer( goto_programt::targett check = dest.add( goto_programt::make_incomplete_goto(condition, target->source_location())); - goto_programt::targett invalidate = dest.add(goto_programt::instructiont( - static_cast(get_nil_irep()), - target->source_location(), - ASSIGN, - nil_exprt(), - {})); + const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr()); + const dereference_exprt deref( + b_plus_i, to_type_with_subtype(buf_type).subtype()); + + const side_effect_expr_nondett nondet( + to_type_with_subtype(buf_type).subtype(), target->source_location()); + + // invalidate + dest.add( + goto_programt::make_assignment(deref, nondet, target->source_location())); const plus_exprt plus( cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type())); @@ -880,13 +885,4 @@ void string_instrumentationt::invalidate_buffer( dest.add(goto_programt::make_skip(target->source_location())); check->complete_goto(exit); - - const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr()); - const dereference_exprt deref( - b_plus_i, to_type_with_subtype(buf_type).subtype()); - - const side_effect_expr_nondett nondet( - to_type_with_subtype(buf_type).subtype(), target->source_location()); - - invalidate->code_nonconst() = code_assignt(deref, nondet); } diff --git a/unit/goto-checker/report_util/is_property_less_than.cpp b/unit/goto-checker/report_util/is_property_less_than.cpp index 536459d55c3..fca7802da02 100644 --- a/unit/goto-checker/report_util/is_property_less_than.cpp +++ b/unit/goto-checker/report_util/is_property_less_than.cpp @@ -12,9 +12,13 @@ static goto_programt::instructiont instruction_for_location( location.set_file(file); location.set_function(function); location.set_line(line_no); - goto_programt::instructiont instruction; - instruction.source_location_nonconst() = location; - return instruction; + + return goto_programt::instructiont{ + codet{ID_nil}, + location, + goto_program_instruction_typet::NO_INSTRUCTION_TYPE, + {}, + {}}; } static property_infot test_info(const goto_programt::const_targett &target) diff --git a/unit/goto-programs/structured_trace_util.cpp b/unit/goto-programs/structured_trace_util.cpp index 9725a3ba1b5..e2f847efcaa 100644 --- a/unit/goto-programs/structured_trace_util.cpp +++ b/unit/goto-programs/structured_trace_util.cpp @@ -22,9 +22,13 @@ goto_programt::targett add_instruction( const source_locationt &location, goto_programt::instructionst &instructions) { - goto_programt::instructiont instruction; + goto_programt::instructiont instruction{ + codet{ID_nil}, + location, + goto_program_instruction_typet::NO_INSTRUCTION_TYPE, + {}, + {}}; instruction.location_number = instructions.size(); - instruction.source_location_nonconst() = location; instructions.push_back(instruction); return std::next(instructions.begin(), instruction.location_number); }