replace direct access to goto_instructiont::guard

Author: kroening

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

@@ -195,7 +195,7 @@ void variable_sensitivity_dependence_domaint::data_dependencies(
   }
   else if(to->is_goto())
   {
-    eval_data_deps(to->guard, ns, domain_data_deps);
+    eval_data_deps(to->condition(), ns, domain_data_deps);
   }
 }
 

src/goto-checker/symex_bmc.cpp

@@ -57,7 +57,7 @@ void symex_bmct::symex_step(
 
   if(
     !state.guard.is_false() && state.source.pc->is_assume() &&
-    simplify_expr(state.source.pc->guard, ns).is_false())
+    simplify_expr(state.source.pc->condition(), ns).is_false())
   {
     log.statistics() << "aborting path on assume(false) at "
                      << state.source.pc->source_location << " thread "
@@ -86,7 +86,7 @@ void symex_bmct::symex_step(
     // sure the goto is considered covered
     if(
       cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
-      cur_pc->guard.is_true())
+      cur_pc->condition().is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
@@ -109,7 +109,7 @@ void symex_bmct::merge_goto(
     // could the branch possibly be taken?
     !prev_guard.is_false() && !state.guard.is_false() &&
     // branches only, no single-successor goto
-    !prev_pc->guard.is_true())
+    !prev_pc->condition().is_true())
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 

src/goto-instrument/cover_instrument_branch.cpp

@@ -25,7 +25,8 @@ void cover_branch_instrumentert::instrument(
 
   const bool is_function_entry_point =
     i_it == goto_program.instructions.begin();
-  const bool is_conditional_goto = i_it->is_goto() && !i_it->guard.is_true();
+  const bool is_conditional_goto =
+    i_it->is_goto() && !i_it->condition().is_true();
   if(!is_function_entry_point && !is_conditional_goto)
     return;
 
@@ -52,7 +53,7 @@ void cover_branch_instrumentert::instrument(
     std::string true_comment = "block " + b + " branch true";
     std::string false_comment = "block " + b + " branch false";
 
-    exprt guard = i_it->guard;
+    exprt guard = i_it->condition();
     source_locationt source_location = i_it->source_location;
 
     goto_program.insert_before_swap(i_it);

src/goto-programs/goto_convert.cpp

@@ -876,7 +876,7 @@ void goto_convertt::convert_loop_contracts(
     }
 
     PRECONDITION(loop->is_goto());
-    loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
+    loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
   }
 
   if(!decreases_clause.is_nil())
@@ -889,7 +889,7 @@ void goto_convertt::convert_loop_contracts(
     }
 
     PRECONDITION(loop->is_goto());
-    loop->guard.add(ID_C_spec_decreases).swap(decreases_clause);
+    loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
   }
 }
 

src/goto-programs/remove_virtual_functions.cpp

@@ -421,8 +421,8 @@ static goto_programt::targett replace_virtual_function_with_dispatch_table(
           !new_code_gotos.empty(),
           "a dispatch table entry has been processed already, "
           "which should have created a GOTO");
-        new_code_gotos.instructions.back().guard =
-          or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
+        new_code_gotos.instructions.back().condition_nonconst() = or_exprt(
+          new_code_gotos.instructions.back().condition(), class_id_test);
       }
       else
       {

src/goto-programs/show_goto_functions_json.cpp

@@ -95,11 +95,11 @@ json_objectt show_goto_functions_jsont::convert(
           instruction_entry["operands"] = std::move(operand_array);
         }
 
-        if(!instruction.guard.is_true())
+        if(instruction.has_condition())
         {
-          json_objectt guard_object=
+          json_objectt guard_object =
             no_comments_irep_converter.convert_from_irep(
-              instruction.guard);
+              instruction.condition());
 
           instruction_entry["guard"] = std::move(guard_object);
         }

src/goto-programs/write_goto_binary.cpp

@@ -98,7 +98,11 @@ bool write_goto_binary(
         irepconverter.reference_convert(instruction.get_code(), out);
         irepconverter.reference_convert(instruction.source_location, out);
         write_gb_word(out, (long)instruction.type);
-        irepconverter.reference_convert(instruction.guard, out);
+
+        const auto condition =
+          instruction.has_condition() ? instruction.condition() : true_exprt();
+        irepconverter.reference_convert(condition, out);
+
         write_gb_word(out, instruction.target_number);
 
         write_gb_word(out, instruction.targets.size());