remove goto_programt::get_ and set_condition

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())
     {

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,16 +790,15 @@ 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;
         }
 
         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);
 

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

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:

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
       }

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:

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);

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);
     }

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)

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:

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)

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?

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())

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

src/goto-analyzer/taint_analysis.cpp

@@ -333,17 +333,15 @@ 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;
         }
 
         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;
 

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())
     {

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
     {

src/goto-instrument/accelerate/all_paths_enumerator.cpp

@@ -134,15 +134,15 @@ 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();
         ++it)
     {
       if(next == *it)
       {
-        guard = t->get_condition();
+        guard = t->condition();
         break;
       }
     }

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;
     }

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -810,15 +810,15 @@ 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();
           ++it)
       {
         if(next==*it)
         {
-          cond = t->get_condition();
+          cond = t->condition();
           break;
         }
       }

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);
 }

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
     {

src/goto-instrument/accelerate/sat_path_enumerator.cpp

@@ -161,15 +161,15 @@ 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();
           ++it)
       {
         if(next==*it)
         {
-          cond = t->get_condition();
+          cond = t->condition();
           break;
         }
       }