introduce non-const instructiont::get_condition()

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

Author: Daniel Kroening

src/analyses/constant_propagator.cpp

@@ -756,11 +756,12 @@ 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);
+      replace_types_rec(d.values.replace_const, it->get_condition());
+      constant_propagator_domaint::partial_evaluate(
+        d.values, it->get_condition(), ns);
     }
     else if(it->is_assign())
     {

src/goto-programs/adjust_float_expressions.cpp

@@ -202,7 +202,7 @@ void adjust_float_expressions(
     adjust_float_expressions(it->code, ns);
 
     if(it->has_condition())
-      adjust_float_expressions(it->guard, ns);
+      adjust_float_expressions(it->get_condition(), ns);
   }
 }
 

src/goto-programs/goto_inline_class.cpp

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

src/goto-programs/goto_program.h

@@ -287,6 +287,13 @@ class goto_programt
       return guard;
     }
 
+    /// Get the condition of gotos, assume, assert
+    exprt &get_condition()
+    {
+      PRECONDITION(has_condition());
+      return guard;
+    }
+
     // 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,7 @@ static void rename_symbols_in_function(
     rename_symbol(iit->code);
 
     if(iit->has_condition())
-      rename_symbol(iit->guard);
+      rename_symbol(iit->get_condition());
   }
 }
 

src/goto-programs/remove_complex.cpp

@@ -290,7 +290,7 @@ static void remove_complex(
     remove_complex(it->code);
 
     if(it->has_condition())
-      remove_complex(it->guard);
+      remove_complex(it->get_condition());
   }
 }
 

src/goto-programs/remove_vector.cpp

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

src/goto-programs/rewrite_union.cpp

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

src/pointer-analysis/goto_program_dereference.cpp

@@ -302,7 +302,8 @@ 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);
+    dereference_expr(
+      i.get_condition(), checks_only, value_set_dereferencet::modet::READ);
 
   if(i.is_assign())
   {