use instructiont::get_condition()

This will eventually enable use to protect instructiont::guard.

Author: Daniel Kroening

src/analyses/goto_rw.cpp

@@ -762,7 +762,10 @@ void goto_rw(
   case ASSUME:
   case ASSERT:
     rw_set.get_objects_rec(
-      function, target, rw_range_sett::get_modet::READ, target->guard);
+      function,
+      target,
+      rw_range_sett::get_modet::READ,
+      target->get_condition());
     break;
 
   case RETURN:

src/analyses/local_cfg.cpp

@@ -48,7 +48,7 @@ void local_cfgt::build(const goto_programt &goto_program)
     switch(instruction.type)
     {
     case GOTO:
-      if(!instruction.guard.is_true())
+      if(!instruction.get_condition().is_true())
         node.successors.push_back(loc_nr+1);
 
       for(const auto &target : instruction.targets)

src/goto-analyzer/static_verifier.cpp

@@ -256,7 +256,7 @@ bool static_verifier(
       if(!i_it->is_assert())
         continue;
 
-      exprt e(i_it->guard);
+      exprt e(i_it->get_condition());
       auto dp = ai.abstract_state_before(i_it);
       const ai_domain_baset &domain(*dp);
       domain.ai_simplify(e, ns);

src/goto-analyzer/taint_analysis.cpp

@@ -334,13 +334,16 @@ bool taint_analysist::operator()(
       {
         if(!i_it->is_assert())
           continue;
-        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(custom_bitvector_analysis[i_it].has_values.is_false())
           continue;
 
-        exprt result=custom_bitvector_analysis.eval(i_it->guard, i_it);
+        exprt result =
+          custom_bitvector_analysis.eval(i_it->get_condition(), i_it);
         exprt result2=simplify_expr(result, ns);
 
         if(result2.is_true())

src/goto-instrument/accelerate/accelerate.cpp

@@ -43,11 +43,10 @@ goto_programt::targett acceleratet::find_back_jump(
       ++it)
   {
     goto_programt::targett t=*it;
-    if(t->is_goto() &&
-        t->guard.is_true() &&
-        t->targets.size()==1 &&
-        t->targets.front()==loop_header &&
-        t->location_number > back_jump->location_number)
+    if(
+      t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
+      t->targets.front() == loop_header &&
+      t->location_number > back_jump->location_number)
     {
       back_jump=t;
     }

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -276,7 +276,7 @@ exprt acceleration_utilst::precondition(patht &path)
     }
     else if(t->is_assume() || t->is_assert())
     {
-      ret=implies_exprt(t->guard, ret);
+      ret = implies_exprt(t->get_condition(), ret);
     }
     else
     {

src/goto-instrument/accelerate/all_paths_enumerator.cpp

@@ -136,15 +136,15 @@ void all_paths_enumeratort::extend_path(
 
   if(t->is_goto())
   {
-    guard=not_exprt(t->guard);
+    guard = not_exprt(t->get_condition());
 
     for(goto_programt::targetst::iterator it=t->targets.begin();
         it != t->targets.end();
         ++it)
     {
       if(next == *it)
       {
-        guard=t->guard;
+        guard = t->get_condition();
         break;
       }
     }

src/goto-instrument/accelerate/cone_of_influence.cpp

@@ -87,7 +87,7 @@ void cone_of_influencet::get_succs(
 
   if(rit->is_goto())
   {
-    if(!rit->guard.is_false())
+    if(!rit->get_condition().is_false())
     {
       // Branch can be taken.
       for(goto_programt::targetst::const_iterator t=rit->targets.begin();
@@ -100,14 +100,14 @@ void cone_of_influencet::get_succs(
       }
     }
 
-    if(rit->guard.is_true())
+    if(rit->get_condition().is_true())
     {
       return;
     }
   }
   else if(rit->is_assume() || rit->is_assert())
   {
-    if(rit->guard.is_false())
+    if(rit->get_condition().is_false())
     {
       return;
     }

src/goto-instrument/branch.cpp

@@ -45,11 +45,10 @@ void branch(
       // T': id("not-taken");   t3
       // ...
 
-      if(i_it->is_goto() &&
-         !i_it->guard.is_constant())
+      if(i_it->is_goto() && !i_it->get_condition().is_constant())
       {
         // negate condition
-        i_it->guard = boolean_negate(i_it->guard);
+        i_it->guard = boolean_negate(i_it->get_condition());
 
         goto_programt::targett t1=body.insert_after(i_it);
         t1->make_function_call(

src/goto-programs/goto_convert.cpp

@@ -254,8 +254,10 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
 
     if(
       it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
-      !it_goto_y->guard.is_true() || it_goto_y->is_target())
+      !it_goto_y->get_condition().is_true() || it_goto_y->is_target())
+    {
       continue;
+    }
 
     auto it_z = std::next(it_goto_y);
 
@@ -266,7 +268,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
     if(it->get_target()->target_number == it_z->target_number)
     {
       it->set_target(it_goto_y->get_target());
-      it->guard = boolean_negate(it->guard);
+      it->guard = boolean_negate(it->get_condition());
       it_goto_y->make_skip();
     }
   }
@@ -554,9 +556,9 @@ void goto_convertt::convert_block(
 
   // see if we need to do any destructors -- may have been processed
   // in a prior break/continue/return already, don't create dead code
-  if(!dest.empty() &&
-     dest.instructions.back().is_goto() &&
-     dest.instructions.back().guard.is_true())
+  if(
+    !dest.empty() && dest.instructions.back().is_goto() &&
+    dest.instructions.back().get_condition().is_true())
   {
     // don't do destructors when we are unreachable
   }
@@ -1474,10 +1476,10 @@ 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().guard.is_false() &&
-     true_case.instructions.back().labels.empty())
+  if(
+    is_size_one(true_case) && true_case.instructions.back().is_assert() &&
+    true_case.instructions.back().get_condition().is_false() &&
+    true_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
     // if(some) { label: assert(false); }
@@ -1492,10 +1494,10 @@ 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().guard.is_false() &&
-     false_case.instructions.back().labels.empty())
+  if(
+    is_size_one(false_case) && false_case.instructions.back().is_assert() &&
+    false_case.instructions.back().get_condition().is_false() &&
+    false_case.instructions.back().labels.empty())
   {
     // The above conjunction deliberately excludes the instance
     // if(some) ... else { label: assert(false); }
@@ -1514,7 +1516,7 @@ 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().guard.is_false() &&
+    true_case.instructions.front().get_condition().is_false() &&
     true_case.instructions.front().labels.empty() &&
     true_case.instructions.back().labels.empty())
   {

src/goto-programs/goto_convert_functions.cpp

@@ -109,9 +109,12 @@ void goto_convert_functionst::add_return(
     while(true)
     {
       // unconditional goto, say from while(1)?
-      if(last_instruction->is_goto() &&
-         last_instruction->guard.is_true())
+      if(
+        last_instruction->is_goto() &&
+        last_instruction->get_condition().is_true())
+      {
         return;
+      }
 
       // return?
       if(last_instruction->is_return())

src/goto-programs/goto_program.cpp

@@ -73,10 +73,9 @@ std::ostream &goto_programt::output_instruction(
     break;
 
   case GOTO:
-    if(!instruction.guard.is_true())
+    if(!instruction.get_condition().is_true())
     {
-      out << "IF "
-          << from_expr(ns, identifier, instruction.guard)
+      out << "IF " << from_expr(ns, identifier, instruction.get_condition())
           << " THEN ";
     }
 
@@ -112,7 +111,7 @@ std::ostream &goto_programt::output_instruction(
       out << "ASSERT ";
 
     {
-      out << from_expr(ns, identifier, instruction.guard);
+      out << from_expr(ns, identifier, instruction.get_condition());
 
       const irep_idt &comment=instruction.source_location.get_comment();
       if(comment!="")
@@ -276,7 +275,7 @@ std::list<exprt> expressions_read(
   case ASSUME:
   case ASSERT:
   case GOTO:
-    dest.push_back(instruction.guard);
+    dest.push_back(instruction.get_condition());
     break;
 
   case RETURN:
@@ -416,9 +415,9 @@ std::string as_string(
     return "(NO INSTRUCTION TYPE)";
 
   case GOTO:
-    if(!i.guard.is_true())
+    if(!i.get_condition().is_true())
     {
-      result += "IF " + from_expr(ns, function, i.guard) + " THEN ";
+      result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN ";
     }
 
     result+="GOTO ";
@@ -449,7 +448,7 @@ std::string as_string(
     else
       result+="ASSERT ";
 
-    result += from_expr(ns, function, i.guard);
+    result += from_expr(ns, function, i.get_condition());
 
     {
       const irep_idt &comment=i.source_location.get_comment();
@@ -634,7 +633,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.guard.is_true())
+    if(i.is_assert() && !i.get_condition().is_true())
       return true;
 
   return false;

src/goto-programs/goto_trace.cpp

@@ -116,7 +116,7 @@ void goto_trace_stept::output(
       if(!comment.empty())
         out << "  " << comment << '\n';
 
-      out << "  " << format(pc->guard) << '\n';
+      out << "  " << format(pc->get_condition()) << '\n';
       out << '\n';
     }
   }
@@ -388,7 +388,8 @@ void show_compact_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+          out << "  "
+              << from_expr(ns, step.function_id, step.pc->get_condition())
               << '\n';
         }
 
@@ -511,7 +512,8 @@ void show_full_goto_trace(
 
         if(step.pc->is_assert())
         {
-          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+          out << "  "
+              << from_expr(ns, step.function_id, step.pc->get_condition())
               << '\n';
         }
 
@@ -529,7 +531,8 @@ void show_full_goto_trace(
 
         if(step.pc->is_assume())
         {
-          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+          out << "  "
+              << from_expr(ns, step.function_id, step.pc->get_condition())
               << '\n';
         }
 

src/goto-programs/graphml_witness.cpp

@@ -160,7 +160,7 @@ static bool filter_out(
      prev_it->pc->source_location==it->pc->source_location)
     return true;
 
-  if(it->is_goto() && it->pc->guard.is_true())
+  if(it->is_goto() && it->pc->get_condition().is_true())
     return true;
 
   const source_locationt &source_location=it->pc->source_location;
@@ -376,12 +376,12 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
   {
     const source_locationt &source_location=it->source.pc->source_location;
 
-    if(it->hidden ||
-       (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
-       (it->is_goto() && it->source.pc->guard.is_true()) ||
-       source_location.is_nil() ||
-       source_location.is_built_in() ||
-       source_location.get_line().empty())
+    if(
+      it->hidden ||
+      (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
+      (it->is_goto() && it->source.pc->get_condition().is_true()) ||
+      source_location.is_nil() || source_location.is_built_in() ||
+      source_location.get_line().empty())
     {
       step_to_node[step_nr]=sink;
 

src/goto-programs/instrument_preconditions.cpp

@@ -117,7 +117,7 @@ void instrument_preconditions(
         for(const auto &p : preconditions)
         {
           goto_program.insert_before_swap(it);
-          exprt instance=p->guard;
+          exprt instance = p->get_condition();
           r(instance);
           it->make_assertion(instance);
           it->source_location=source_location;

src/goto-programs/interpreter.cpp

@@ -368,7 +368,7 @@ void interpretert::step()
 /// executes a goto instruction
 void interpretert::execute_goto()
 {
-  if(evaluate_boolean(pc->guard))
+  if(evaluate_boolean(pc->get_condition()))
   {
     if(pc->targets.empty())
       throw "taken goto without target";
@@ -728,13 +728,13 @@ void interpretert::assign(
 
 void interpretert::execute_assume()
 {
-  if(!evaluate_boolean(pc->guard))
+  if(!evaluate_boolean(pc->get_condition()))
     throw "assumption failed";
 }
 
 void interpretert::execute_assert()
 {
-  if(!evaluate_boolean(pc->guard))
+  if(!evaluate_boolean(pc->get_condition()))
   {
     if((target_assert==pc) || stop_on_assertion)
       throw "program assertion reached";