introduce instructiont::set_condition()

This will eventually allow us to protect the guard data member.

Author: Daniel Kroening

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/goto-instrument/branch.cpp

@@ -48,7 +48,7 @@ void branch(
       if(i_it->is_goto() && !i_it->get_condition().is_constant())
       {
         // negate condition
-        i_it->guard = boolean_negate(i_it->get_condition());
+        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

@@ -202,7 +202,11 @@ void adjust_float_expressions(
     adjust_float_expressions(it->code, ns);
 
     if(it->has_condition())
-      adjust_float_expressions(it->guard, ns);
+    {
+      exprt c = it->get_condition();
+      adjust_float_expressions(c, ns);
+      it->set_condition(c);
+    }
   }
 }
 

src/goto-programs/goto_convert.cpp

@@ -268,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->get_condition());
+      it->set_condition(boolean_negate(it->get_condition()));
       it_goto_y->make_skip();
     }
   }

src/goto-programs/goto_inline_class.cpp

@@ -318,7 +318,11 @@ void goto_inlinet::insert_function_body(
       replace_location(it->code, target->source_location);
 
       if(it->has_condition())
-        replace_location(it->guard, target->source_location);
+      {
+        exprt c = it->get_condition();
+        replace_location(c, target->source_location);
+        it->set_condition(c);
+      }
     }
   }
 

src/goto-programs/goto_program.h

@@ -271,7 +271,7 @@ class goto_programt
     goto_program_instruction_typet type;
 
     /// Guard for gotos, assume, assert
-    /// Use get_condition() to read
+    /// Use get_condition() to read, and set_condition(c) to write.
     exprt guard;
 
     /// Does this instruction have a condition?
@@ -287,6 +287,13 @@ class goto_programt
       return guard;
     }
 
+    /// Set the condition of gotos, assume, assert
+    void set_condition(exprt c)
+    {
+      PRECONDITION(has_condition());
+      guard = std::move(c);
+    }
+
     // The below will eventually become a single target only.
     /// The target for gotos and for start_thread nodes
     typedef std::list<instructiont>::iterator targett;

src/goto-programs/link_goto_model.cpp

@@ -35,7 +35,11 @@ static void rename_symbols_in_function(
     rename_symbol(iit->code);
 
     if(iit->has_condition())
-      rename_symbol(iit->guard);
+    {
+      exprt c = iit->get_condition();
+      rename_symbol(c);
+      iit->set_condition(c);
+    }
   }
 }
 

src/goto-programs/remove_complex.cpp

@@ -290,7 +290,11 @@ static void remove_complex(
     remove_complex(it->code);
 
     if(it->has_condition())
-      remove_complex(it->guard);
+    {
+      exprt c = it->get_condition();
+      remove_complex(c);
+      it->set_condition(c);
+    }
   }
 }
 

src/goto-programs/remove_vector.cpp

@@ -223,7 +223,11 @@ void remove_vector(goto_functionst::goto_functiont &goto_function)
     remove_vector(it->code);
 
     if(it->has_condition())
-      remove_vector(it->guard);
+    {
+      exprt c = it->get_condition();
+      remove_vector(c);
+      it->set_condition(c);
+    }
   }
 }
 

src/goto-programs/rewrite_union.cpp

@@ -106,7 +106,11 @@ void rewrite_union(goto_functionst::goto_functiont &goto_function)
     rewrite_union(it->code);
 
     if(it->has_condition())
-      rewrite_union(it->guard);
+    {
+      exprt c = it->get_condition();
+      rewrite_union(c);
+      it->set_condition(c);
+    }
   }
 }
 

src/pointer-analysis/goto_program_dereference.cpp

@@ -302,7 +302,11 @@ void goto_program_dereferencet::dereference_instruction(
   goto_programt::instructiont &i=*target;
 
   if(i.has_condition())
-    dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);
+  {
+    exprt c = i.get_condition();
+    dereference_expr(c, checks_only, value_set_dereferencet::modet::READ);
+    i.set_condition(c);
+  }
 
   if(i.is_assign())
   {