use instructiont::get_condition()

Author: Daniel Kroening

src/analyses/constant_propagator.cpp

@@ -169,7 +169,7 @@ void constant_propagator_domaint::transform(
   }
   else if(from->is_assume())
   {
-    two_way_propagate_rec(from->guard, ns, cp);
+    two_way_propagate_rec(from->get_condition(), ns, cp);
   }
   else if(from->is_goto())
   {
@@ -178,9 +178,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->guard;
+      g = from->get_condition();
     else
-      g = not_exprt(from->guard);
+      g = not_exprt(from->get_condition());
     partial_evaluate(values, g, ns);
     if(g.is_false())
      values.set_to_bottom();

src/analyses/custom_bitvector_analysis.cpp

@@ -520,9 +520,9 @@ void custom_bitvector_domaint::transform(
     break;
 
   case GOTO:
-    if(has_get_must_or_may(instruction.guard))
+    if(has_get_must_or_may(instruction.get_condition()))
     {
-      exprt guard=instruction.guard;
+      exprt guard = instruction.get_condition();
 
       // Comparing iterators is safe as the target must be within the same list
       // of instructions because this is a GOTO.
@@ -776,13 +776,14 @@ void custom_bitvector_analysist::check(
 
       if(i_it->is_assert())
       {
-        if(!custom_bitvector_domaint::has_get_must_or_may(i_it->guard))
+        if(!custom_bitvector_domaint::has_get_must_or_may(
+             i_it->get_condition()))
           continue;
 
         if(operator[](i_it).has_values.is_false())
           continue;
 
-        exprt tmp=eval(i_it->guard, i_it);
+        exprt tmp = eval(i_it->get_condition(), i_it);
         const namespacet ns(goto_model.symbol_table);
         result=simplify_expr(tmp, ns);
 

src/analyses/flow_insensitive_analysis.cpp

@@ -24,14 +24,10 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
 {
   if(!from->is_goto())
     return true_exprt();
-
-  locationt next=from;
-  next++;
-
-  if(next==to)
-    return boolean_negate(from->guard);
-
-  return from->guard;
+  else if(std::next(from) == to)
+    return boolean_negate(from->get_condition());
+  else
+    return from->get_condition();
 }
 
 exprt flow_insensitive_abstract_domain_baset::get_return_lhs(locationt to) const

src/analyses/interval_domain.cpp

@@ -88,15 +88,15 @@ void interval_domaint::transform(
       if(from->get_target() != next) // If equal then a skip
       {
         if(next == to)
-          assume(not_exprt(instruction.guard), ns);
+          assume(not_exprt(instruction.get_condition()), ns);
         else
-          assume(instruction.guard, ns);
+          assume(instruction.get_condition(), ns);
       }
     }
     break;
 
   case ASSUME:
-    assume(instruction.guard, ns);
+    assume(instruction.get_condition(), ns);
     break;
 
   case FUNCTION_CALL:

src/analyses/invariant_propagation.cpp

@@ -253,7 +253,7 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
 
     const invariant_sett &invariant_set = d.invariant_set;
 
-    exprt simplified_guard(i_it->guard);
+    exprt simplified_guard(i_it->get_condition());
 
     invariant_set.simplify(simplified_guard);
     ::simplify(simplified_guard, ns);

src/analyses/invariant_set_domain.cpp

@@ -28,12 +28,10 @@ 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->guard);
+      exprt tmp(from_l->get_condition());
 
-      goto_programt::const_targett next=from_l;
-      next++;
-      if(next==to_l)
-        tmp = boolean_negate(from_l->guard);
+      if(std::next(from_l) == to_l)
+        tmp = boolean_negate(from_l->get_condition());
 
       simplify(tmp, ns);
       invariant_set.strengthen(tmp);
@@ -43,7 +41,7 @@ void invariant_set_domaint::transform(
   case ASSERT:
   case ASSUME:
     {
-      exprt tmp(from_l->guard);
+      exprt tmp(from_l->get_condition());
       simplify(tmp, ns);
       invariant_set.strengthen(tmp);
     }

src/analyses/local_safe_pointers.cpp

@@ -126,7 +126,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 
     // Possible checks:
     case ASSUME:
-      if(auto assume_check = get_null_checked_expr(instruction.guard))
+      if(auto assume_check = get_null_checked_expr(instruction.get_condition()))
       {
         if(assume_check->checked_when_taken)
           checked_expressions.insert(assume_check->checked_expr);
@@ -147,7 +147,9 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
         // merge point and everything will be assumed maybe-null in any case.
         if(target_emplace_result.second)
         {
-          if(auto conditional_check = get_null_checked_expr(instruction.guard))
+          if(
+            auto conditional_check =
+              get_null_checked_expr(instruction.get_condition()))
           {
             // Add the GOTO condition to either the target or current state,
             // as appropriate:

src/analyses/static_analysis.cpp

@@ -32,9 +32,9 @@ exprt static_analysis_baset::get_guard(
   next++;
 
   if(next==to)
-    return boolean_negate(from->guard);
+    return boolean_negate(from->get_condition());
 
-  return from->guard;
+  return from->get_condition();
 }
 
 exprt static_analysis_baset::get_return_lhs(locationt to)

src/goto-programs/cfg.h

@@ -218,8 +218,9 @@ void cfg_baset<T, P, I>::compute_edges_goto(
   goto_programt::const_targett next_PC,
   entryt &entry)
 {
-  if(next_PC!=goto_program.instructions.end() &&
-     !instruction.guard.is_true())
+  if(
+    next_PC != goto_program.instructions.end() &&
+    !instruction.get_condition().is_true())
     this->add_edge(entry, entry_map[next_PC]);
 
   this->add_edge(entry, entry_map[instruction.get_target()]);
@@ -400,7 +401,7 @@ void cfg_baset<T, P, I>::compute_edges(
 
   case ASSUME:
     // false guard -> no successor
-    if(instruction.guard.is_false())
+    if(instruction.get_condition().is_false())
       break;
 
   case ASSIGN:

src/goto-programs/goto_program.h

@@ -1030,7 +1030,7 @@ std::list<Target> goto_programt::get_successors(
   {
     std::list<Target> successors(i.targets.begin(), i.targets.end());
 
-    if(!i.guard.is_true() && next!=instructions.end())
+    if(!i.get_condition().is_true() && next != instructions.end())
       successors.push_back(next);
 
     return successors;
@@ -1060,10 +1060,9 @@ std::list<Target> goto_programt::get_successors(
 
   if(i.is_assume())
   {
-    return
-      !i.guard.is_false() && next!=instructions.end() ?
-      std::list<Target>{next} :
-      std::list<Target>();
+    return !i.get_condition().is_false() && next != instructions.end()
+             ? std::list<Target>{next}
+             : std::list<Target>();
   }
 
   if(next!=instructions.end())

src/goto-symex/symex_goto.cpp

@@ -34,7 +34,7 @@ void goto_symext::symex_goto(statet &state)
     return; // nothing to do
   }
 
-  exprt old_guard=instruction.guard;
+  exprt old_guard = instruction.get_condition();
   clean_expr(old_guard, state, false);
 
   exprt new_guard=old_guard;

src/goto-symex/symex_main.cpp

@@ -408,7 +408,7 @@ void goto_symext::symex_step(
   case ASSUME:
     if(!state.guard.is_false())
     {
-      exprt tmp=instruction.guard;
+      exprt tmp = instruction.get_condition();
       clean_expr(tmp, state, false);
       state.rename(tmp, ns);
       symex_assume(state, tmp);
@@ -423,7 +423,7 @@ void goto_symext::symex_step(
       std::string msg=id2string(state.source.pc->source_location.get_comment());
       if(msg=="")
         msg="assertion";
-      exprt tmp(instruction.guard);
+      exprt tmp(instruction.get_condition());
       clean_expr(tmp, state, false);
       vcc(tmp, msg, state);
     }