introduce instructiont::has_condition()

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

Author: Daniel Kroening

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

@@ -393,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-programs/adjust_float_expressions.cpp

@@ -200,7 +200,9 @@ 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())
+      adjust_float_expressions(it->guard, ns);
   }
 }
 

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

@@ -315,8 +315,10 @@ 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())
+        replace_location(it->guard, target->source_location);
     }
   }
 

src/goto-programs/goto_program.h

@@ -274,10 +274,16 @@ class goto_programt
     /// Use get_condition() to read
     exprt guard;
 
+    /// Does this instruction have a condition?
+    bool has_condition() const
+    {
+      return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
+    }
+
     /// Get the condition of gotos, assume, assert
     const exprt &get_condition() const
     {
-      PRECONDITION(is_goto() || is_assume() || is_assert());
+      PRECONDITION(has_condition());
       return guard;
     }
 

src/goto-programs/link_goto_model.cpp

@@ -33,7 +33,9 @@ static void rename_symbols_in_function(
   Forall_goto_program_instructions(iit, program)
   {
     rename_symbol(iit->code);
-    rename_symbol(iit->guard);
+
+    if(iit->has_condition())
+      rename_symbol(iit->guard);
   }
 }
 
@@ -144,7 +146,9 @@ static bool link_functions(
       Forall_goto_program_instructions(iit, dest_it->second.body)
       {
         object_type_updates(iit->code);
-        object_type_updates(iit->guard);
+
+        if(iit->has_condition())
+          object_type_updates(iit->guard);
       }
   }
 

src/goto-programs/remove_complex.cpp

@@ -288,7 +288,9 @@ static void remove_complex(
   Forall_goto_program_instructions(it, goto_function.body)
   {
     remove_complex(it->code);
-    remove_complex(it->guard);
+
+    if(it->has_condition())
+      remove_complex(it->guard);
   }
 }
 

src/goto-programs/remove_vector.cpp

@@ -221,7 +221,9 @@ void remove_vector(goto_functionst::goto_functiont &goto_function)
   Forall_goto_program_instructions(it, goto_function.body)
   {
     remove_vector(it->code);
-    remove_vector(it->guard);
+
+    if(it->has_condition())
+      remove_vector(it->guard);
   }
 }
 

src/goto-programs/rewrite_union.cpp

@@ -104,7 +104,9 @@ void rewrite_union(goto_functionst::goto_functiont &goto_function)
   Forall_goto_program_instructions(it, goto_function.body)
   {
     rewrite_union(it->code);
-    rewrite_union(it->guard);
+
+    if(it->has_condition())
+      rewrite_union(it->guard);
   }
 }
 

src/goto-programs/slice_global_inits.cpp

@@ -67,8 +67,12 @@ void slice_global_inits(goto_modelt &goto_model)
     {
       const codet &code = i_it->code;
       find_symbols(code, symbols, true, false);
-      const exprt &expr = i_it->guard;
-      find_symbols(expr, symbols, true, false);
+
+      if(i_it->has_condition())
+      {
+        const exprt &expr = i_it->get_condition();
+        find_symbols(expr, symbols, true, false);
+      }
     }
   }
 

src/pointer-analysis/goto_program_dereference.cpp

@@ -301,7 +301,8 @@ void goto_program_dereferencet::dereference_instruction(
   #endif
   goto_programt::instructiont &i=*target;
 
-  dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);
+  if(i.has_condition())
+    dereference_expr(i.guard, checks_only, value_set_dereferencet::modet::READ);
 
   if(i.is_assign())
   {