avoid accesses to instructiont::guard

src/analyses/constant_propagator.cpp

@@ -756,11 +756,13 @@ void constant_propagator_ait::replace(
       continue;
 
     replace_types_rec(d.values.replace_const, it->code);
-    replace_types_rec(d.values.replace_const, it->guard);
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
-      constant_propagator_domaint::partial_evaluate(d.values, it->guard, ns);
+      exprt c = it->get_condition();
+      replace_types_rec(d.values.replace_const, c);
+      constant_propagator_domaint::partial_evaluate(d.values, c, ns);
+      it->set_condition(c);
     }
     else if(it->is_assign())
     {

src/analyses/dirty.cpp

@@ -20,7 +20,9 @@ void dirtyt::build(const goto_functiont &goto_function)
   forall_goto_program_instructions(it, goto_function.body)
   {
     find_dirty(it->code);
-    find_dirty(it->guard);
+
+    if(it->has_condition())
+      find_dirty(it->get_condition());
   }
 }
 

src/analyses/goto_check.cpp

@@ -1671,7 +1671,8 @@ void goto_checkt::goto_check(
        i.is_target())
       assertions.clear();
 
-    check(i.guard);
+    if(i.has_condition())
+      check(i.get_condition());
 
     // magic ERROR label?
     for(const auto &label : error_labels)

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,18 @@ 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;
     }
@@ -394,7 +393,8 @@ void acceleratet::add_dirty_checks()
     // the right hand side of an assignment.  Assume each is not dirty.
     find_symbols_sett read;
 
-    find_symbols(it->guard, read);
+    if(it->has_condition())
+      find_symbols(it->get_condition(), read);
 
     if(it->is_assign())
     {

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->set_condition(boolean_negate(i_it->get_condition()));
 
         goto_programt::targett t1=body.insert_after(i_it);
         t1->make_function_call(

src/goto-programs/adjust_float_expressions.cpp

@@ -200,7 +200,13 @@ void adjust_float_expressions(
   Forall_goto_program_instructions(it, goto_function.body)
   {
     adjust_float_expressions(it->code, ns);
-    adjust_float_expressions(it->guard, ns);
+
+    if(it->has_condition())
+    {
+      exprt c = it->get_condition();
+      adjust_float_expressions(c, ns);
+      it->set_condition(c);
+    }
   }
 }
 

src/goto-programs/compute_called_functions.cpp

@@ -56,7 +56,9 @@ void compute_address_taken_functions(
 {
   forall_goto_program_instructions(it, goto_program)
   {
-    compute_address_taken_functions(it->guard, address_taken);
+    if(it->has_condition())
+      compute_address_taken_functions(it->get_condition(), address_taken);
+
     compute_address_taken_functions(it->code, address_taken);
   }
 }

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->set_condition(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_inline_class.cpp

@@ -315,8 +315,14 @@ void goto_inlinet::insert_function_body(
     Forall_goto_program_instructions(it, tmp)
     {
       replace_location(it->source_location, target->source_location);
-      replace_location(it->guard, target->source_location);
       replace_location(it->code, target->source_location);
+
+      if(it->has_condition())
+      {
+        exprt c = it->get_condition();
+        replace_location(c, target->source_location);
+        it->set_condition(c);
+      }
     }
   }
 

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;