From a25657d37c718c17bdddd2afe2b1a97912552862 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 12 May 2022 16:49:27 -0700 Subject: [PATCH] remove goto_programt::get_ and set_condition This removes to methods that have been deprecated since October 2021, together with its remaining uses. --- src/analyses/constant_propagator.cpp | 10 ++++----- src/analyses/custom_bitvector_analysis.cpp | 9 ++++---- src/analyses/flow_insensitive_analysis.cpp | 4 ++-- src/analyses/goto_rw.cpp | 5 +---- src/analyses/interval_analysis.cpp | 2 +- src/analyses/interval_domain.cpp | 6 ++--- src/analyses/invariant_propagation.cpp | 2 +- src/analyses/invariant_set_domain.cpp | 4 ++-- src/analyses/local_cfg.cpp | 2 +- src/analyses/local_safe_pointers.cpp | 4 ++-- src/analyses/static_analysis.cpp | 4 ++-- src/ansi-c/goto_check_c.cpp | 2 +- src/goto-analyzer/static_simplifier.cpp | 12 +++++----- src/goto-analyzer/static_verifier.cpp | 2 +- src/goto-analyzer/taint_analysis.cpp | 6 ++--- src/goto-instrument/accelerate/accelerate.cpp | 4 ++-- .../accelerate/acceleration_utils.cpp | 2 +- .../accelerate/all_paths_enumerator.cpp | 4 ++-- .../accelerate/cone_of_influence.cpp | 6 ++--- .../disjunctive_polynomial_acceleration.cpp | 4 ++-- .../accelerate/overflow_instrumenter.cpp | 2 +- .../accelerate/polynomial_accelerator.cpp | 2 +- .../accelerate/sat_path_enumerator.cpp | 4 ++-- .../accelerate/scratch_program.cpp | 6 ++--- src/goto-instrument/branch.cpp | 4 ++-- src/goto-instrument/call_sequences.cpp | 2 +- src/goto-instrument/contracts/contracts.cpp | 8 +++---- src/goto-instrument/contracts/utils.cpp | 2 +- src/goto-instrument/cover.cpp | 2 +- .../cover_instrument_assume.cpp | 2 +- src/goto-instrument/dot.cpp | 14 ++++++------ src/goto-instrument/full_slicer.cpp | 2 +- .../generate_function_bodies.cpp | 4 ++-- .../goto_instrument_parse_options.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 4 ++-- src/goto-instrument/nondet_volatile.cpp | 5 ++--- src/goto-instrument/rw_set.cpp | 2 +- src/goto-instrument/unwind.cpp | 8 +++---- src/goto-instrument/wmm/weak_memory.cpp | 4 ++-- src/goto-programs/cfg.h | 4 ++-- src/goto-programs/goto_convert.cpp | 16 +++++++------- src/goto-programs/goto_convert_functions.cpp | 4 +--- src/goto-programs/goto_program.cpp | 22 +++++++++---------- src/goto-programs/goto_program.h | 20 ++--------------- src/goto-programs/goto_trace.cpp | 10 ++++----- src/goto-programs/graphml_witness.cpp | 4 ++-- .../instrument_preconditions.cpp | 2 +- src/goto-programs/interpreter.cpp | 6 ++--- src/goto-programs/link_goto_model.cpp | 6 +---- src/goto-programs/remove_skip.cpp | 4 ++-- .../remove_virtual_functions.cpp | 2 +- src/goto-programs/rewrite_union.cpp | 6 +---- src/goto-programs/show_properties.cpp | 7 +++--- src/goto-programs/string_abstraction.cpp | 9 +++----- src/goto-symex/solver_hardness.cpp | 6 ++--- src/goto-symex/symex_goto.cpp | 6 ++--- src/goto-symex/symex_main.cpp | 4 ++-- .../goto_program_dereference.cpp | 6 +---- src/pointer-analysis/value_set_domain.h | 2 +- unit/goto-instrument/cover_instrument.cpp | 4 ++-- 60 files changed, 139 insertions(+), 184 deletions(-) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 8565cc8f2e3..a75935cc4b5 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -171,7 +171,7 @@ void constant_propagator_domaint::transform( } else if(from->is_assume()) { - two_way_propagate_rec(from->get_condition(), ns, cp); + two_way_propagate_rec(from->condition(), ns, cp); } else if(from->is_goto()) { @@ -180,9 +180,9 @@ void constant_propagator_domaint::transform( // Comparing iterators is safe as the target must be within the same list // of instructions because this is a GOTO. if(from->get_target()==to) - g = from->get_condition(); + g = from->condition(); else - g = not_exprt(from->get_condition()); + g = not_exprt(from->condition()); partial_evaluate(values, g, ns); if(g.is_false()) values.set_to_bottom(); @@ -762,10 +762,10 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { - exprt c = it->get_condition(); + exprt c = it->condition(); replace_types_rec(d.values.replace_const, c); if(!constant_propagator_domaint::partial_evaluate(d.values, c, ns)) - it->set_condition(c); + it->condition_nonconst() = c; } else if(it->is_assign()) { diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index aa1ad2b2ab7..66630c51d7b 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -517,9 +517,9 @@ void custom_bitvector_domaint::transform( break; case GOTO: - if(has_get_must_or_may(instruction.get_condition())) + if(has_get_must_or_may(instruction.condition())) { - exprt guard = instruction.get_condition(); + exprt guard = instruction.condition(); // Comparing iterators is safe as the target must be within the same list // of instructions because this is a GOTO. @@ -790,8 +790,7 @@ void custom_bitvector_analysist::check( if(i_it->is_assert()) { - if(!custom_bitvector_domaint::has_get_must_or_may( - i_it->get_condition())) + if(!custom_bitvector_domaint::has_get_must_or_may(i_it->condition())) { continue; } @@ -799,7 +798,7 @@ void custom_bitvector_analysist::check( if(operator[](i_it).has_values.is_false()) continue; - exprt tmp = eval(i_it->get_condition(), i_it); + exprt tmp = eval(i_it->condition(), i_it); const namespacet ns(goto_model.symbol_table); result = simplify_expr(std::move(tmp), ns); diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index 593a65a8732..171f8de64af 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -23,9 +23,9 @@ exprt flow_insensitive_abstract_domain_baset::get_guard( if(!from->is_goto()) return true_exprt(); else if(std::next(from) == to) - return boolean_negate(from->get_condition()); + return boolean_negate(from->condition()); else - return from->get_condition(); + return from->condition(); } exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 0116f8376fe..865c32daf2a 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -867,10 +867,7 @@ void goto_rw( case ASSUME: case ASSERT: rw_set.get_objects_rec( - function, - target, - rw_range_sett::get_modet::READ, - target->get_condition()); + function, target, rw_range_sett::get_modet::READ, target->condition()); break; case SET_RETURN_VALUE: diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index cc8b3881b13..bbb73fb11e3 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -46,7 +46,7 @@ void instrument_intervals( { goto_programt::const_targett previous = std::prev(i_it); - if(previous->is_goto() && !previous->get_condition().is_true()) + if(previous->is_goto() && !previous->condition().is_true()) { // we follow a branch, instrument } diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index a8a4038f6d1..05090caaa4a 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -91,15 +91,15 @@ void interval_domaint::transform( if(from->get_target() != next) // If equal then a skip { if(next == to) - assume(not_exprt(instruction.get_condition()), ns); + assume(not_exprt(instruction.condition()), ns); else - assume(instruction.get_condition(), ns); + assume(instruction.condition(), ns); } break; } case ASSUME: - assume(instruction.get_condition(), ns); + assume(instruction.condition(), ns); break; case FUNCTION_CALL: diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index fee95383033..ff90f398e9b 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -264,7 +264,7 @@ void invariant_propagationt::simplify(goto_programt &goto_program) const invariant_sett &invariant_set = d.invariant_set; - exprt simplified_guard(i_it->get_condition()); + exprt simplified_guard(i_it->condition()); invariant_set.simplify(simplified_guard); ::simplify(simplified_guard, ns); diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index 03f3df8bbf8..5e28c7d11c2 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -31,7 +31,7 @@ void invariant_set_domaint::transform( { // Comparing iterators is safe as the target must be within the same list // of instructions because this is a GOTO. - exprt tmp(from_l->get_condition()); + exprt tmp(from_l->condition()); if(std::next(from_l) == to_l) tmp = boolean_negate(tmp); @@ -44,7 +44,7 @@ void invariant_set_domaint::transform( case ASSERT: case ASSUME: { - exprt tmp(from_l->get_condition()); + exprt tmp(from_l->condition()); simplify(tmp, ns); invariant_set.strengthen(tmp); } diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 42bb6d8e3de..60bcabb783f 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -35,7 +35,7 @@ void local_cfgt::build(const goto_programt &goto_program) switch(instruction.type()) { case GOTO: - if(!instruction.get_condition().is_true()) + if(!instruction.condition().is_true()) node.successors.push_back(loc_nr+1); for(const auto &target : instruction.targets) diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index 3bb53eff009..2a28bafed44 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -127,7 +127,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) // Possible checks: case ASSUME: - if(auto assume_check = get_null_checked_expr(instruction.get_condition())) + if(auto assume_check = get_null_checked_expr(instruction.condition())) { if(assume_check->checked_when_taken) checked_expressions.insert(assume_check->checked_expr); @@ -150,7 +150,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) { if( auto conditional_check = - get_null_checked_expr(instruction.get_condition())) + get_null_checked_expr(instruction.condition())) { // Add the GOTO condition to either the target or current state, // as appropriate: diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index f21fa593aa0..5fe9b201231 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -27,9 +27,9 @@ exprt static_analysis_baset::get_guard( if(!from->is_goto()) return true_exprt(); else if(std::next(from) == to) - return boolean_negate(from->get_condition()); + return boolean_negate(from->condition()); else - return from->get_condition(); + return from->condition(); } exprt static_analysis_baset::get_return_lhs(locationt to) diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 6a8492275c0..d54833e869b 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -2085,7 +2085,7 @@ void goto_check_ct::goto_check( if(i.has_condition()) { - check(i.get_condition()); + check(i.condition()); } // magic ERROR label? diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index ade080ed950..974126a0c15 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -65,7 +65,7 @@ bool static_simplifier( if(i_it->is_assert()) { - exprt cond = i_it->get_condition(); + exprt cond = i_it->condition(); bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns); @@ -74,12 +74,12 @@ bool static_simplifier( else { simplified.asserts++; - i_it->set_condition(cond); + i_it->condition_nonconst() = cond; } } else if(i_it->is_assume()) { - exprt cond = i_it->get_condition(); + exprt cond = i_it->condition(); bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns); @@ -88,12 +88,12 @@ bool static_simplifier( else { simplified.assumes++; - i_it->set_condition(cond); + i_it->condition_nonconst() = cond; } } else if(i_it->is_goto()) { - exprt cond = i_it->get_condition(); + exprt cond = i_it->condition(); bool unchanged = ai.abstract_state_before(i_it)->ai_simplify(cond, ns); @@ -102,7 +102,7 @@ bool static_simplifier( else { simplified.gotos++; - i_it->set_condition(cond); + i_it->condition_nonconst() = cond; } } else if(i_it->is_assign()) diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index 768f4e5c35c..9e9282f6de7 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -115,7 +115,7 @@ static_verifier_resultt::static_verifier_resultt( const namespacet &ns) { PRECONDITION(assert_location->is_assert()); - exprt e(assert_location->get_condition()); + exprt e(assert_location->condition()); // If there are multiple, distinct histories that reach the same location // we can get better results by checking with each individually rather diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index d229d885c95..f47a93dc54c 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -333,8 +333,7 @@ bool taint_analysist::operator()( if(!i_it->is_assert()) continue; - if(!custom_bitvector_domaint::has_get_must_or_may( - i_it->get_condition())) + if(!custom_bitvector_domaint::has_get_must_or_may(i_it->condition())) { continue; } @@ -342,8 +341,7 @@ bool taint_analysist::operator()( if(custom_bitvector_analysis[i_it].has_values.is_false()) continue; - exprt result = - custom_bitvector_analysis.eval(i_it->get_condition(), i_it); + exprt result = custom_bitvector_analysis.eval(i_it->condition(), i_it); if(simplify_expr(std::move(result), ns).is_true()) continue; diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 782c0b91edd..561b051af52 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -40,7 +40,7 @@ goto_programt::targett acceleratet::find_back_jump( for(const auto &t : loop) { if( - t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 && + t->is_goto() && t->condition().is_true() && t->targets.size() == 1 && t->targets.front() == loop_header && t->location_number > back_jump->location_number) { @@ -382,7 +382,7 @@ void acceleratet::add_dirty_checks() find_symbols_sett read; if(it->has_condition()) - find_symbols_or_nexts(it->get_condition(), read); + find_symbols_or_nexts(it->condition(), read); if(it->is_assign()) { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 8ab1885a6f5..35213de9107 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -250,7 +250,7 @@ exprt acceleration_utilst::precondition(patht &path) } else if(t->is_assume() || t->is_assert()) { - ret = implies_exprt(t->get_condition(), ret); + ret = implies_exprt(t->condition(), ret); } else { diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp index e2463798746..4cc36844cce 100644 --- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp +++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp @@ -134,7 +134,7 @@ void all_paths_enumeratort::extend_path( if(t->is_goto()) { - guard = not_exprt(t->get_condition()); + guard = not_exprt(t->condition()); for(goto_programt::targetst::iterator it=t->targets.begin(); it != t->targets.end(); @@ -142,7 +142,7 @@ void all_paths_enumeratort::extend_path( { if(next == *it) { - guard = t->get_condition(); + guard = t->condition(); break; } } diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp index 1c7f060587e..0c71748e4b9 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.cpp +++ b/src/goto-instrument/accelerate/cone_of_influence.cpp @@ -83,7 +83,7 @@ void cone_of_influencet::get_succs( if(rit->is_goto()) { - if(!rit->get_condition().is_false()) + if(!rit->condition().is_false()) { // Branch can be taken. for(goto_programt::targetst::const_iterator t=rit->targets.begin(); @@ -96,14 +96,14 @@ void cone_of_influencet::get_succs( } } - if(rit->get_condition().is_true()) + if(rit->condition().is_true()) { return; } } else if(rit->is_assume() || rit->is_assert()) { - if(rit->get_condition().is_false()) + if(rit->condition().is_false()) { return; } diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index d0a28fbb6bb..1c136096343 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -810,7 +810,7 @@ void disjunctive_polynomial_accelerationt::build_path( // If this was a conditional branch (it probably was), figure out // if we hit the "taken" or "not taken" branch & accumulate the // appropriate guard. - cond = not_exprt(t->get_condition()); + cond = not_exprt(t->condition()); for(goto_programt::targetst::iterator it=t->targets.begin(); it!=t->targets.end(); @@ -818,7 +818,7 @@ void disjunctive_polynomial_accelerationt::build_path( { if(next==*it) { - cond = t->get_condition(); + cond = t->condition(); break; } } diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp index ef10af8e53c..f69ce37bbc2 100644 --- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp +++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp @@ -64,7 +64,7 @@ void overflow_instrumentert::add_overflow_checks( } if(t->has_condition()) - add_overflow_checks(t, t->get_condition(), added); + add_overflow_checks(t, t->condition(), added); checked.insert(t->location_number); } diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index c7e7114486d..ff0d49d6281 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -780,7 +780,7 @@ exprt polynomial_acceleratort::precondition(patht &path) } else if(t->is_assume() || t->is_assert()) { - ret = implies_exprt(t->get_condition(), ret); + ret = implies_exprt(t->condition(), ret); } else { diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 28c3963995f..2af0f685264 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -161,7 +161,7 @@ void sat_path_enumeratort::build_path( // If this was a conditional branch (it probably was), figure out // if we hit the "taken" or "not taken" branch & accumulate the // appropriate guard. - cond = not_exprt(t->get_condition()); + cond = not_exprt(t->condition()); for(goto_programt::targetst::iterator it=t->targets.begin(); it!=t->targets.end(); @@ -169,7 +169,7 @@ void sat_path_enumeratort::build_path( { if(next==*it) { - cond = t->get_condition(); + cond = t->condition(); break; } } diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 2cce8f0437a..eb739bf4a50 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -155,9 +155,7 @@ void scratch_programt::fix_types() } else if(it->is_assume() || it->is_assert()) { - exprt cond = it->get_condition(); - ::fix_types(cond); - it->set_condition(cond); + ::fix_types(it->condition_nonconst()); } } } @@ -181,7 +179,7 @@ void scratch_programt::append_path(patht &path) } else if(it->loc->is_assert()) { - add(goto_programt::make_assumption(it->loc->get_condition())); + add(goto_programt::make_assumption(it->loc->condition())); } } } diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp index 82ddc987ea8..23670abcd0a 100644 --- a/src/goto-instrument/branch.cpp +++ b/src/goto-instrument/branch.cpp @@ -47,10 +47,10 @@ void branch( // T': id("not-taken"); t3 // ... - if(i_it->is_goto() && !i_it->get_condition().is_constant()) + if(i_it->is_goto() && !i_it->condition().is_constant()) { // negate condition - i_it->set_condition(boolean_negate(i_it->get_condition())); + i_it->condition_nonconst() = boolean_negate(i_it->condition()); goto_programt::targett t1 = body.insert_after( i_it, diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index cf9037e0b78..4dc0ffd1da6 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -231,7 +231,7 @@ void check_call_sequencet::operator()() { goto_programt::const_targett t=e.pc->get_target(); - if(e.pc->get_condition().is_true()) + if(e.pc->condition().is_true()) e.pc=t; else { diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 14be16bfd2d..0b395e87042 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -405,7 +405,7 @@ void code_contractst::check_apply_loop_contracts( } // TODO: Fix loop contract handling for do/while loops. - if(loop_end->is_goto() && !loop_end->get_condition().is_true()) + if(loop_end->is_goto() && !loop_end->condition().is_true()) { log.error() << "Loop contracts are unsupported on do/while loops: " << loop_head_location << messaget::eom; @@ -524,7 +524,7 @@ void code_contractst::check_apply_loop_contracts( // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume(); - loop_end->set_condition(boolean_negate(loop_end->get_condition())); + loop_end->condition_nonconst() = boolean_negate(loop_end->condition()); std::set seen_targets; // Find all exit points of the loop, make temporary variables `DEAD`, @@ -1060,9 +1060,9 @@ void code_contractst::apply_loop_contract( exprt assigns_clause = static_cast(loop_end->condition().find(ID_C_spec_assigns)); exprt invariant = static_cast( - loop_end->get_condition().find(ID_C_spec_loop_invariant)); + loop_end->condition().find(ID_C_spec_loop_invariant)); exprt decreases_clause = static_cast( - loop_end->get_condition().find(ID_C_spec_decreases)); + loop_end->condition().find(ID_C_spec_decreases)); if(invariant.is_nil()) { diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index acc9ac441e0..f1991846a44 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -165,7 +165,7 @@ void simplify_gotos(goto_programt &goto_program, namespacet &ns) { if( instruction.is_goto() && - simplify_expr(instruction.get_condition(), ns).is_false()) + simplify_expr(instruction.condition(), ns).is_false()) instruction.turn_into_skip(); } } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index c77c98cddc6..ee132d0deec 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -307,7 +307,7 @@ static void instrument_cover_goals( if( successor != function.body.instructions.end() && successor->is_assume() && - successor->get_condition() == i_it->get_condition()) + successor->condition() == i_it->condition()) { successor->turn_into_skip(); } diff --git a/src/goto-instrument/cover_instrument_assume.cpp b/src/goto-instrument/cover_instrument_assume.cpp index 5adee97d61f..bc3a728b11e 100644 --- a/src/goto-instrument/cover_instrument_assume.cpp +++ b/src/goto-instrument/cover_instrument_assume.cpp @@ -25,7 +25,7 @@ void cover_assume_instrumentert::instrument( { const auto location = i_it->source_location(); const auto assume_condition = - expr2c(i_it->get_condition(), namespacet{symbol_tablet()}); + expr2c(i_it->condition(), namespacet{symbol_tablet()}); const auto comment_before = "assert(false) before assume(" + assume_condition + ")"; const auto comment_after = diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index 7bc90b155d1..cc8025b948e 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -106,11 +106,11 @@ void dott::write_dot_subgraph( std::stringstream tmp; if(it->is_goto()) { - if(it->get_condition().is_true()) + if(it->condition().is_true()) tmp.str("Goto"); else { - std::string t = from_expr(ns, function_id, it->get_condition()); + std::string t = from_expr(ns, function_id, it->condition()); while(t[ t.size()-1 ]=='\n') t = t.substr(0, t.size()-1); tmp << escape(t) << "?"; @@ -118,14 +118,14 @@ void dott::write_dot_subgraph( } else if(it->is_assume()) { - std::string t = from_expr(ns, function_id, it->get_condition()); + std::string t = from_expr(ns, function_id, it->condition()); while(t[ t.size()-1 ]=='\n') t = t.substr(0, t.size()-1); tmp << "Assume\\n(" << escape(t) << ")"; } else if(it->is_assert()) { - std::string t = from_expr(ns, function_id, it->get_condition()); + std::string t = from_expr(ns, function_id, it->condition()); while(t[ t.size()-1 ]=='\n') t = t.substr(0, t.size()-1); tmp << "Assert\\n(" << escape(t) << ")"; @@ -178,7 +178,7 @@ void dott::write_dot_subgraph( out << "Node_" << subgraphscount << "_" << it->location_number; out << " [shape="; - if(it->is_goto() && !it->get_condition().is_constant()) + if(it->is_goto() && !it->condition().is_constant()) out << "diamond"; else out <<"Mrecord"; @@ -314,13 +314,13 @@ void dott::find_next( std::set &tres, std::set &fres) { - if(it->is_goto() && !it->get_condition().is_false()) + if(it->is_goto() && !it->condition().is_false()) { for(const auto &target : it->targets) tres.insert(target); } - if(it->is_goto() && it->get_condition().is_true()) + if(it->is_goto() && it->condition().is_true()) return; goto_programt::const_targett next = it; next++; diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 6cc914c18b6..12c9831c4c7 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -281,7 +281,7 @@ void full_slicert::operator()( else if(implicit(instruction)) add_to_queue(queue, instruction_node_index, instruction); else if( - (instruction->is_goto() && instruction->get_condition().is_true()) || + (instruction->is_goto() && instruction->condition().is_true()) || instruction->is_throw()) jumps.push_back(instruction_node_index); else if(instruction->is_decl()) diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 5575a7a20a0..c190795eaee 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -108,7 +108,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest const namespacet ns(symbol_table); std::ostringstream comment_stream; comment_stream << id2string(ID_assertion) << " " - << format(assert_instruction->get_condition()); + << format(assert_instruction->condition()); assert_instruction->source_location_nonconst().set_comment( comment_stream.str()); assert_instruction->source_location_nonconst().set_property_class( @@ -139,7 +139,7 @@ class assert_false_then_assume_false_generate_function_bodiest const namespacet ns(symbol_table); std::ostringstream comment_stream; comment_stream << id2string(ID_assertion) << " " - << format(assert_instruction->get_condition()); + << format(assert_instruction->condition()); assert_instruction->source_location_nonconst().set_comment( comment_stream.str()); assert_instruction->source_location_nonconst().set_property_class( diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 2e6c727bbba..3b7828cad4e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -662,7 +662,7 @@ int goto_instrument_parse_optionst::doit() log.status() << ins.get_code().pretty() << messaget::eom; if(ins.has_condition()) { - log.status() << "[guard] " << ins.get_condition().pretty() + log.status() << "[guard] " << ins.condition().pretty() << messaget::eom; } } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 2bd751e2480..6a0c16b26bd 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -193,7 +193,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction( case ASSERT: system_headers.insert("assert.h"); - dest.add(code_assertt(target->get_condition())); + dest.add(code_assertt(target->condition())); dest.statements().back().add_source_location().set_comment( target->source_location().get_comment()); return target; @@ -829,7 +829,7 @@ bool goto_program2codet::remove_default( next_case != goto_program.instructions.end() && next_case == default_target && (!it->case_last->is_goto() || - (it->case_last->get_condition().is_true() && + (it->case_last->condition().is_true() && it->case_last->get_target() == default_target))) { // if there is no goto here, yet we got here, all others would diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp index 2d690089aeb..73553c6e2f5 100644 --- a/src/goto-instrument/nondet_volatile.cpp +++ b/src/goto-instrument/nondet_volatile.cpp @@ -253,9 +253,8 @@ void nondet_volatilet::nondet_volatile( else if(instruction.has_condition()) { // do condition - exprt cond = instruction.get_condition(); - nondet_volatile_rhs(symbol_table, cond, pre, post); - instruction.set_condition(cond); + nondet_volatile_rhs( + symbol_table, instruction.condition_nonconst(), pre, post); } const auto pre_size = pre.instructions.size(); diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index 9507b2fc9a4..8c348e73303 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -53,7 +53,7 @@ void _rw_set_loct::compute() target->is_assume() || target->is_assert()) { - read(target->get_condition()); + read(target->condition()); } else if(target->is_function_call()) { diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 35add96a40f..f03c2a36a73 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -139,14 +139,14 @@ void goto_unwindt::unwind( exprt exit_cond = false_exprt(); // default is false - if(!t->get_condition().is_true()) // cond in backedge + if(!t->condition().is_true()) // cond in backedge { - exit_cond = boolean_negate(t->get_condition()); + exit_cond = boolean_negate(t->condition()); } else if(loop_head->is_goto()) { if(loop_head->get_target()==loop_exit) // cond in forward edge - exit_cond = loop_head->get_condition(); + exit_cond = loop_head->condition(); } if( @@ -184,7 +184,7 @@ void goto_unwindt::unwind( goto_programt::const_targett t_before=loop_exit; t_before--; - if(!t_before->is_goto() || !t_before->get_condition().is_true()) + if(!t_before->is_goto() || !t_before->condition().is_true()) { goto_programt::targett t_goto = goto_program.insert_before( loop_exit, diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index fc3317ce6e4..0e4946b5337 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -88,11 +88,11 @@ void introduce_temporaries( symbol_exprt symbol_expr=new_symbol.symbol_expr(); goto_programt::instructiont new_i = goto_programt::make_assignment( - code_assignt(symbol_expr, instruction.get_condition()), + code_assignt(symbol_expr, instruction.condition()), instruction.source_location()); // replace guard - instruction.set_condition(symbol_expr); + instruction.condition_nonconst() = symbol_expr; goto_program.insert_before_swap(i_it, new_i); i_it++; // step forward diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index 97c94c9c74d..e271d761b19 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -320,7 +320,7 @@ void cfg_baset::compute_edges_goto( { if( next_PC != goto_program.instructions.end() && - !instruction.get_condition().is_true()) + !instruction.condition().is_true()) { this->add_edge(entry, entry_map[next_PC]); } @@ -501,7 +501,7 @@ void cfg_baset::compute_edges( case ASSUME: // false guard -> no successor - if(instruction.get_condition().is_false()) + if(instruction.condition().is_false()) break; case ASSIGN: diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 92ca061523e..55567c9bb24 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -256,7 +256,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest) if( it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() || - !it_goto_y->get_condition().is_true() || it_goto_y->is_target()) + !it_goto_y->condition().is_true() || it_goto_y->is_target()) { continue; } @@ -559,7 +559,7 @@ void goto_convertt::convert_block( // in a prior break/continue/return already, don't create dead code if( !dest.empty() && dest.instructions.back().is_goto() && - dest.instructions.back().get_condition().is_true()) + dest.instructions.back().condition().is_true()) { // don't do destructors when we are unreachable } @@ -1527,12 +1527,12 @@ void goto_convertt::generate_ifthenelse( // do guarded assertions directly if( is_size_one(true_case) && true_case.instructions.back().is_assert() && - true_case.instructions.back().get_condition().is_false() && + true_case.instructions.back().condition().is_false() && true_case.instructions.back().labels.empty()) { // The above conjunction deliberately excludes the instance // if(some) { label: assert(false); } - true_case.instructions.back().set_condition(boolean_negate(guard)); + true_case.instructions.back().condition_nonconst() = boolean_negate(guard); dest.destructive_append(true_case); true_case.instructions.clear(); if( @@ -1545,12 +1545,12 @@ void goto_convertt::generate_ifthenelse( // similarly, do guarded assertions directly if( is_size_one(false_case) && false_case.instructions.back().is_assert() && - false_case.instructions.back().get_condition().is_false() && + false_case.instructions.back().condition().is_false() && false_case.instructions.back().labels.empty()) { // The above conjunction deliberately excludes the instance // if(some) ... else { label: assert(false); } - false_case.instructions.back().set_condition(guard); + false_case.instructions.back().condition_nonconst() = guard; dest.destructive_append(false_case); false_case.instructions.clear(); if( @@ -1565,11 +1565,11 @@ void goto_convertt::generate_ifthenelse( if( is_empty(false_case) && true_case.instructions.size() == 2 && true_case.instructions.front().is_assert() && - true_case.instructions.front().get_condition().is_false() && + true_case.instructions.front().condition().is_false() && true_case.instructions.front().labels.empty() && true_case.instructions.back().labels.empty()) { - true_case.instructions.front().set_condition(boolean_negate(guard)); + true_case.instructions.front().condition_nonconst() = boolean_negate(guard); true_case.instructions.erase(--true_case.instructions.end()); dest.destructive_append(true_case); true_case.instructions.clear(); diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index a4ca9ecacba..324b3e84594 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -111,9 +111,7 @@ void goto_convert_functionst::add_return( while(true) { // unconditional goto, say from while(1)? - if( - last_instruction->is_goto() && - last_instruction->get_condition().is_true()) + if(last_instruction->is_goto() && last_instruction->condition().is_true()) { return; } diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 165f9fcfdac..8ef40e45b27 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -91,9 +91,9 @@ std::ostream &goto_programt::output_instruction( case GOTO: case INCOMPLETE_GOTO: - if(!instruction.get_condition().is_true()) + if(!instruction.condition().is_true()) { - out << "IF " << format(instruction.get_condition()) << " THEN "; + out << "IF " << format(instruction.condition()) << " THEN "; } out << "GOTO "; @@ -179,7 +179,7 @@ std::ostream &goto_programt::output_instruction( out << "ASSERT "; { - out << format(instruction.get_condition()); + out << format(instruction.condition()); const irep_idt &comment = instruction.source_location().get_comment(); if(!comment.empty()) @@ -336,7 +336,7 @@ std::list expressions_read( case ASSUME: case ASSERT: case GOTO: - dest.push_back(instruction.get_condition()); + dest.push_back(instruction.condition()); break; case SET_RETURN_VALUE: @@ -492,9 +492,9 @@ std::string as_string( return "(NO INSTRUCTION TYPE)"; case GOTO: - if(!i.get_condition().is_true()) + if(!i.condition().is_true()) { - result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN "; + result += "IF " + from_expr(ns, function, i.condition()) + " THEN "; } result+="GOTO "; @@ -525,7 +525,7 @@ std::string as_string( else result+="ASSERT "; - result += from_expr(ns, function, i.get_condition()); + result += from_expr(ns, function, i.condition()); { const irep_idt &comment = i.source_location().get_comment(); @@ -712,7 +712,7 @@ void goto_programt::copy_from(const goto_programt &src) bool goto_programt::has_assertion() const { for(const auto &i : instructions) - if(i.is_assert() && !i.get_condition().is_true()) + if(i.is_assert() && !i.condition().is_true()) return true; return false; @@ -1049,9 +1049,9 @@ void goto_programt::instructiont::transform( case NO_INSTRUCTION_TYPE: if(has_condition()) { - auto new_condition = f(get_condition()); + auto new_condition = f(condition()); if(new_condition.has_value()) - set_condition(new_condition.value()); + condition_nonconst() = new_condition.value(); } } } @@ -1104,7 +1104,7 @@ void goto_programt::instructiont::apply( case INCOMPLETE_GOTO: case NO_INSTRUCTION_TYPE: if(has_condition()) - f(get_condition()); + f(condition()); } } diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 87be6590b5a..28c5292f323 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -362,22 +362,6 @@ class goto_programt return is_goto() || is_incomplete_goto() || is_assume() || is_assert(); } - /// Get the condition of gotos, assume, assert - DEPRECATED(SINCE(2021, 10, 12, "Use condition() instead")) - const exprt &get_condition() const - { - PRECONDITION(has_condition()); - return guard; - } - - /// Set the condition of gotos, assume, assert - DEPRECATED(SINCE(2021, 10, 12, "Use condition_nonconst() instead")) - void set_condition(exprt c) - { - PRECONDITION(has_condition()); - guard = std::move(c); - } - /// Get the condition of gotos, assume, assert const exprt &condition() const { @@ -1122,7 +1106,7 @@ std::list goto_programt::get_successors( { std::list successors(i.targets.begin(), i.targets.end()); - if(!i.get_condition().is_true() && next != instructions.end()) + if(!i.condition().is_true() && next != instructions.end()) successors.push_back(next); return successors; @@ -1152,7 +1136,7 @@ std::list goto_programt::get_successors( if(i.is_assume()) { - return !i.get_condition().is_false() && next != instructions.end() + return !i.condition().is_false() && next != instructions.end() ? std::list{next} : std::list(); } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 6886580a9f9..c4ba7003589 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -128,7 +128,7 @@ void goto_trace_stept::output( if(!comment.empty()) out << " " << comment << '\n'; - out << " " << format(pc->get_condition()) << '\n'; + out << " " << format(pc->condition()) << '\n'; out << '\n'; } } @@ -422,8 +422,7 @@ void show_compact_goto_trace( if(step.pc->is_assert()) { - out << " " - << from_expr(ns, step.function_id, step.pc->get_condition()) + out << " " << from_expr(ns, step.function_id, step.pc->condition()) << '\n'; } @@ -550,8 +549,7 @@ void show_full_goto_trace( if(step.pc->is_assert()) { - out << " " - << from_expr(ns, step.function_id, step.pc->get_condition()) + out << " " << from_expr(ns, step.function_id, step.pc->condition()) << '\n'; } @@ -568,7 +566,7 @@ void show_full_goto_trace( if(!step.pc->source_location().is_nil()) out << " " << step.pc->source_location() << '\n'; - out << " " << from_expr(ns, step.function_id, step.pc->get_condition()) + out << " " << from_expr(ns, step.function_id, step.pc->condition()) << '\n'; } break; diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 6ffd6b73216..b83e192ef0c 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -246,7 +246,7 @@ static bool filter_out( prev_it->pc->source_location() == it->pc->source_location()) return true; - if(it->is_goto() && it->pc->get_condition().is_true()) + if(it->is_goto() && it->pc->condition().is_true()) return true; const source_locationt &source_location = it->pc->source_location(); @@ -551,7 +551,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) if( it->hidden || (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || - (it->is_goto() && it->source.pc->get_condition().is_true()) || + (it->is_goto() && it->source.pc->condition().is_true()) || source_location.is_nil() || source_location.is_built_in() || source_location.get_line().empty()) { diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp index 10c4409f2dc..9cd2a07f3b8 100644 --- a/src/goto-programs/instrument_preconditions.cpp +++ b/src/goto-programs/instrument_preconditions.cpp @@ -127,7 +127,7 @@ void instrument_preconditions( for(const auto &p : preconditions) { goto_program.insert_before_swap(it); - exprt instance = p->get_condition(); + exprt instance = p->condition(); r(instance); *it = goto_programt::make_assertion(instance, source_location); it->source_location_nonconst().set_property_class( diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 7e0b2316620..f93ab27d0e5 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -369,7 +369,7 @@ void interpretert::step() /// executes a goto instruction void interpretert::execute_goto() { - if(evaluate_boolean(pc->get_condition())) + if(evaluate_boolean(pc->condition())) { if(pc->targets.empty()) throw "taken goto without target"; @@ -720,13 +720,13 @@ void interpretert::assign( void interpretert::execute_assume() { - if(!evaluate_boolean(pc->get_condition())) + if(!evaluate_boolean(pc->condition())) throw "assumption failed"; } void interpretert::execute_assert() { - if(!evaluate_boolean(pc->get_condition())) + if(!evaluate_boolean(pc->condition())) { if(show) output.error() << "assertion failed at " << pc->location_number << "\n" diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 09124bd67ea..75141785e53 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -37,11 +37,7 @@ static void rename_symbols_in_function( rename_symbol(instruction.code_nonconst()); if(instruction.has_condition()) - { - exprt c = instruction.get_condition(); - rename_symbol(c); - instruction.set_condition(c); - } + rename_symbol(instruction.condition_nonconst()); } } diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 1a5d59f0947..5e213840233 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -37,7 +37,7 @@ bool is_skip( if(it->is_goto()) { - if(it->get_condition().is_false()) + if(it->condition().is_false()) return true; goto_programt::const_targett next_it = it; @@ -48,7 +48,7 @@ bool is_skip( // A branch to the next instruction is a skip // We also require the guard to be 'true' - return it->get_condition().is_true() && it->get_target() == next_it; + return it->condition().is_true() && it->get_target() == next_it; } if(it->is_other()) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index e5aa4a0e02f..8e30fb8a890 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -164,7 +164,7 @@ static goto_programt analyse_checks_directly_preceding_function_call( break; } - exprt guard = instr_it->get_condition(); + exprt guard = instr_it->condition(); bool changed = false; for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end(); diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp index 714c9568a0f..2f109083618 100644 --- a/src/goto-programs/rewrite_union.cpp +++ b/src/goto-programs/rewrite_union.cpp @@ -102,11 +102,7 @@ void rewrite_union(goto_functionst::goto_functiont &goto_function) rewrite_union(instruction.code_nonconst()); if(instruction.has_condition()) - { - exprt c = instruction.get_condition(); - rewrite_union(c); - instruction.set_condition(c); - } + rewrite_union(instruction.condition_nonconst()); } } diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index a0e795f607b..90be11961c2 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -78,7 +78,7 @@ void show_properties( xml_property.new_element("description").data=id2string(description); xml_property.new_element("expression").data = - from_expr(ns, identifier, ins.get_condition()); + from_expr(ns, identifier, ins.condition()); const irept &basic_block_lines = source_location.get_basic_block_source_lines(); @@ -112,7 +112,7 @@ void show_properties( msg.result() << " " << ins.source_location() << '\n' << " " << description << '\n' - << " " << from_expr(ns, identifier, ins.get_condition()) + << " " << from_expr(ns, identifier, ins.condition()) << '\n'; msg.result() << messaget::eom; @@ -149,8 +149,7 @@ void convert_properties_json( {"class", json_stringt(property_class)}, {"sourceLocation", json(source_location)}, {"description", json_stringt(description)}, - {"expression", - json_stringt(from_expr(ns, identifier, ins.get_condition()))}}; + {"expression", json_stringt(from_expr(ns, identifier, ins.condition()))}}; const irept &basic_block_lines = source_location.get_basic_block_source_lines(); diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 508f4572471..6b98b4df0b6 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -474,12 +474,9 @@ goto_programt::targett string_abstractiont::abstract( case GOTO: case ASSERT: case ASSUME: - if(has_string_macros(it->get_condition())) - { - exprt tmp = it->get_condition(); - replace_string_macros(tmp, false, it->source_location()); - it->set_condition(tmp); - } + if(has_string_macros(it->condition())) + replace_string_macros( + it->condition_nonconst(), false, it->source_location()); break; case FUNCTION_CALL: diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp index de589f814e7..9c75a200af1 100644 --- a/src/goto-symex/solver_hardness.cpp +++ b/src/goto-symex/solver_hardness.cpp @@ -244,9 +244,9 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) case GOTO: case INCOMPLETE_GOTO: - if(!instruction.get_condition().is_true()) + if(!instruction.condition().is_true()) { - out << "IF " << format(instruction.get_condition()) << " THEN "; + out << "IF " << format(instruction.condition()) << " THEN "; } out << "GOTO "; @@ -287,7 +287,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) else out << "ASSERT "; - out << format(instruction.get_condition()); + out << format(instruction.condition()); break; case SKIP: diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 0ac08cd361a..5439cc6a228 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -233,7 +233,7 @@ void goto_symext::symex_goto(statet &state) const goto_programt::instructiont &instruction=*state.source.pc; - exprt new_guard = clean_expr(instruction.get_condition(), state, false); + exprt new_guard = clean_expr(instruction.condition(), state, false); renamedt renamed_guard = state.rename(std::move(new_guard), ns); renamed_guard = try_evaluate_pointer_comparisons( @@ -471,7 +471,7 @@ void goto_symext::symex_goto(statet &state) state, taken_state, not_taken_state, - instruction.get_condition(), + instruction.condition(), new_guard, ns); } @@ -572,7 +572,7 @@ void goto_symext::symex_unreachable_goto(statet &state) goto_state_list.emplace_back(state.source, std::move(new_state)); }; - if(instruction.get_condition().is_true()) + if(instruction.condition().is_true()) { if(instruction.is_backwards_goto()) { diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 7df69db080d..648de566760 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -156,7 +156,7 @@ void goto_symext::symex_assert( const goto_programt::instructiont &instruction, statet &state) { - exprt condition = clean_expr(instruction.get_condition(), state, false); + exprt condition = clean_expr(instruction.condition(), state, false); // First, push negations in and perhaps convert existential quantifiers into // universals: @@ -648,7 +648,7 @@ void goto_symext::execute_next_instruction( case ASSUME: if(state.reachable) - symex_assume(state, instruction.get_condition()); + symex_assume(state, instruction.condition()); symex_transition(state); break; diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 3e7f03b39e9..672f749c576 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -200,11 +200,7 @@ void goto_program_dereferencet::dereference_instruction( goto_programt::instructiont &i=*target; if(i.has_condition()) - { - exprt c = i.get_condition(); - dereference_expr(c, checks_only); - i.set_condition(c); - } + dereference_expr(i.condition_nonconst(), checks_only); if(i.is_assign()) { diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index a256718694f..a77154ebcd3 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -92,7 +92,7 @@ void value_set_domain_templatet::transform( break; case ASSUME: - value_set.guard(from_l->get_condition(), ns); + value_set.guard(from_l->condition(), ns); break; case FUNCTION_CALL: diff --git a/unit/goto-instrument/cover_instrument.cpp b/unit/goto-instrument/cover_instrument.cpp index f717e3f4434..cdaa958de73 100644 --- a/unit/goto-instrument/cover_instrument.cpp +++ b/unit/goto-instrument/cover_instrument.cpp @@ -25,7 +25,7 @@ TEST_CASE("cover_intrument_end_of_function", "[core]") REQUIRE(goto_program.instructions.size() == 4); const auto newly_inserted = std::next(goto_program.instructions.begin(), 2); REQUIRE(newly_inserted->is_assert()); - REQUIRE(newly_inserted->get_condition() == false_exprt{}); + REQUIRE(newly_inserted->condition() == false_exprt{}); REQUIRE(newly_inserted->source_location().get_function() == "foo"); } @@ -48,6 +48,6 @@ TEST_CASE("cover_instrument_end_of_function with custom expression", "[core]") REQUIRE(goto_program.instructions.size() == 4); const auto newly_inserted = std::next(goto_program.instructions.begin(), 2); REQUIRE(newly_inserted->is_assert()); - REQUIRE(newly_inserted->get_condition() == true_exprt{}); + REQUIRE(newly_inserted->condition() == true_exprt{}); REQUIRE(newly_inserted->source_location().get_function() == "foo"); }