Merge pull request #6853 from diffblue/protect_guard

kroening · web-flow · commit 44273a34ba46 · 2022-05-17T11:58:33.000+01:00
protect goto_instructiont::guard
diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp
@@ -368,7 +368,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         struct_tag_typet type(stack_catch[i][j].first);
 
         java_instanceof_exprt check(exc_thrown, type);
-        t_exc->guard=check;
+        t_exc->condition_nonconst() = check;
 
         if(remove_added_instanceof)
         {
diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -243,7 +243,8 @@ bool remove_instanceoft::lower_instanceof(
 {
   if(
     target->is_target() &&
-    (contains_instanceof(target->code()) || contains_instanceof(target->guard)))
+    (contains_instanceof(target->code()) ||
+     (target->has_condition() && contains_instanceof(target->condition()))))
   {
     // If this is a branch target, add a skip beforehand so we can splice new
     // GOTO programs before the target instruction without inserting into the
@@ -256,8 +257,12 @@ bool remove_instanceoft::lower_instanceof(
 
   return lower_instanceof(
            function_identifier, target->code_nonconst(), goto_program, target) |
-         lower_instanceof(
-           function_identifier, target->guard, goto_program, target);
+         (target->has_condition() ? lower_instanceof(
+                                      function_identifier,
+                                      target->condition_nonconst(),
+                                      goto_program,
+                                      target)
+                                  : false);
 }
 
 /// Replace every instanceof in the passed function body with an explicit
diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp
@@ -71,7 +71,7 @@ static bool is_call_to(
 
 static bool is_assume_false(goto_programt::const_targett inst)
 {
-  return inst->is_assume() && inst->guard.is_false();
+  return inst->is_assume() && inst->condition().is_false();
 }
 
 /// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,7 +90,7 @@ static goto_programt::const_targett interpret_classid_comparison(
   {
     if(pc->type() == GOTO)
     {
-      exprt guard = pc->guard;
+      exprt guard = pc->condition();
       guard = resolve_classid_test(guard, actual_class_id, ns);
       if(guard.is_true())
       {
diff --git a/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp b/jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp
@@ -92,15 +92,20 @@ SCENARIO(
             }
           }
 
-          for(auto it = instrit->guard.depth_begin(),
-                itend = instrit->guard.depth_end();
-              it != itend; ++it)
+          if(instrit->has_condition())
           {
-            if(it->id() == ID_dereference)
+            const auto &condition = instrit->condition();
+
+            for(auto it = condition.depth_begin(),
+                     itend = condition.depth_end();
+                it != itend;
+                ++it)
             {
-              const auto &deref = to_dereference_expr(*it);
-              REQUIRE(
-                safe_pointers.is_safe_dereference(deref, instrit));
+              if(it->id() == ID_dereference)
+              {
+                const auto &deref = to_dereference_expr(*it);
+                REQUIRE(safe_pointers.is_safe_dereference(deref, instrit));
+              }
             }
           }
         }
diff --git a/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp b/jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp
@@ -71,11 +71,12 @@ SCENARIO(
             // branching for class C and one for class D or O.
             if(instruction.type() == goto_program_instruction_typet::GOTO)
             {
-              if(instruction.guard.id() == ID_equal)
+              if(instruction.condition().id() == ID_equal)
               {
                 THEN("Class C should call its specific method")
                 {
-                  const equal_exprt &eq_expr = to_equal_expr(instruction.guard);
+                  const equal_exprt &eq_expr =
+                    to_equal_expr(instruction.condition());
                   check_function_call(
                     eq_expr,
                     "java::C",
@@ -84,11 +85,12 @@ SCENARIO(
                 }
               }
 
-              else if(instruction.guard.id() == ID_or)
+              else if(instruction.condition().id() == ID_or)
               {
                 THEN("Classes D and O should both call O.toString()")
                 {
-                  const or_exprt &disjunction = to_or_expr(instruction.guard);
+                  const or_exprt &disjunction =
+                    to_or_expr(instruction.condition());
                   REQUIRE(
                     (disjunction.op0().id() == ID_equal &&
                      disjunction.op1().id() == ID_equal));
diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
@@ -50,7 +50,7 @@ void instrument_intervals(
       {
         // we follow a branch, instrument
       }
-      else if(previous->is_function_call() && !previous->guard.is_true())
+      else if(previous->is_function_call())
       {
         // we follow a function call, instrument
       }
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
@@ -79,13 +79,13 @@ void variable_sensitivity_domaint::transform(
         if(to == from->get_target())
         {
           // The AI is exploring the branch where the jump is taken
-          assume(instruction.guard, ns);
+          assume(instruction.condition(), ns);
         }
         else
         {
           // Exploring the path where the jump is not taken - therefore assume
           // the condition is false
-          assume(not_exprt(instruction.guard), ns);
+          assume(not_exprt(instruction.condition()), ns);
         }
       }
       // ignore jumps to the next line, we can assume nothing
@@ -94,7 +94,7 @@ void variable_sensitivity_domaint::transform(
   break;
 
   case ASSUME:
-    assume(instruction.guard, ns);
+    assume(instruction.condition(), ns);
     break;
 
   case FUNCTION_CALL:
diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp
@@ -258,8 +258,11 @@ int linker_script_merget::pointerize_linker_defined_symbols(
     goto_programt &program=gf.second.body;
     for(auto &instruction : program.instructions)
     {
-      for(exprt *insts : std::list<exprt *>(
-            {&(instruction.code_nonconst()), &(instruction.guard)}))
+      std::list<exprt *> expressions = {&instruction.code_nonconst()};
+      if(instruction.has_condition())
+        expressions.push_back(&instruction.condition_nonconst());
+
+      for(exprt *insts : expressions)
       {
         std::list<symbol_exprt> to_pointerize;
         symbols_to_pointerize(linker_values, *insts, to_pointerize);
diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp
@@ -214,7 +214,7 @@ void goto_program_coverage_recordt::compute_coverage_lines(
       it->is_end_function())
       continue;
 
-    const bool is_branch = it->is_goto() && !it->guard.is_constant();
+    const bool is_branch = it->is_goto() && !it->condition().is_constant();
 
     unsigned l =
       safe_string2unsigned(id2string(it->source_location().get_line()));
diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp
@@ -165,7 +165,7 @@ void memory_snapshot_harness_generatort::add_init_section(
   auto ins_it1 = goto_program.insert_before(
     start_it,
     goto_programt::make_goto(goto_program.const_cast_target(start_it)));
-  ins_it1->guard = func_init_done_var;
+  ins_it1->condition_nonconst() = func_init_done_var;
 
   auto ins_it2 = goto_program.insert_after(
     ins_it1,
diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp
@@ -21,7 +21,9 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
     return {};
 
   const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
-  if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
+  if(
+    in_t->is_goto() && !in_t->is_backwards_goto() &&
+    in_t->condition().is_true())
     return block_map[in_t];
 
   return {};
diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp
@@ -40,7 +40,7 @@ void cover_assertion_instrumentert::instrument(
   // turn into 'assert(false)' to avoid simplification
   if(is_non_cover_assertion(i_it))
   {
-    i_it->guard = false_exprt();
+    i_it->condition_nonconst() = false_exprt();
     initialize_source_location(
       i_it, id2string(i_it->source_location().get_comment()), function_id);
   }
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
@@ -199,7 +199,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return target;
 
     case ASSUME:
-      dest.add(code_assumet(target->guard));
+      dest.add(code_assumet(target->condition()));
       return target;
 
     case GOTO:
@@ -514,7 +514,7 @@ goto_programt::const_targett goto_program2codet::convert_do_while(
 {
   assert(loop_end->is_goto() && loop_end->is_backwards_goto());
 
-  code_dowhilet d(loop_end->guard, code_blockt());
+  code_dowhilet d(loop_end->condition(), code_blockt());
   simplify(d.cond(), ns);
 
   copy_source_location(loop_end->targets.front(), d);
@@ -547,7 +547,7 @@ goto_programt::const_targett goto_program2codet::convert_goto(
       (upper_bound==goto_program.instructions.end() ||
        upper_bound->location_number > loop_entry->second->location_number))
     return convert_goto_while(target, loop_entry->second, dest);
-  else if(!target->guard.is_true())
+  else if(!target->condition().is_true())
     return convert_goto_switch(target, upper_bound, dest);
   else if(!loop_last_stack.empty())
     return convert_goto_break_continue(target, upper_bound, dest);
@@ -574,10 +574,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
 
   if(target->get_target()==after_loop)
   {
-    w.cond()=not_exprt(target->guard);
+    w.cond() = not_exprt(target->condition());
     simplify(w.cond(), ns);
   }
-  else if(target->guard.is_true())
+  else if(target->condition().is_true())
   {
     target = convert_goto_goto(target, to_code_block(w.body()));
   }
@@ -594,13 +594,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   loop_last_stack.pop_back();
 
   convert_labels(loop_end, to_code_block(w.body()));
-  if(loop_end->guard.is_false())
+  if(loop_end->condition().is_false())
   {
     to_code_block(w.body()).add(code_breakt());
   }
-  else if(!loop_end->guard.is_true())
+  else if(!loop_end->condition().is_true())
   {
-    code_ifthenelset i(not_exprt(loop_end->guard), code_breakt());
+    code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -661,9 +661,9 @@ goto_programt::const_targett goto_program2codet::get_cases(
       cases_it!=upper_bound && cases_it!=first_target;
       ++cases_it)
   {
-    if(cases_it->is_goto() &&
-       !cases_it->is_backwards_goto() &&
-       cases_it->guard.is_true())
+    if(
+      cases_it->is_goto() && !cases_it->is_backwards_goto() &&
+      cases_it->condition().is_true())
     {
       default_target=cases_it->get_target();
 
@@ -684,16 +684,16 @@ goto_programt::const_targett goto_program2codet::get_cases(
       ++cases_it;
       break;
     }
-    else if(cases_it->is_goto() &&
-            !cases_it->is_backwards_goto() &&
-            (cases_it->guard.id()==ID_equal ||
-             cases_it->guard.id()==ID_or))
+    else if(
+      cases_it->is_goto() && !cases_it->is_backwards_goto() &&
+      (cases_it->condition().id() == ID_equal ||
+       cases_it->condition().id() == ID_or))
     {
       exprt::operandst eqs;
-      if(cases_it->guard.id()==ID_equal)
-        eqs.push_back(cases_it->guard);
+      if(cases_it->condition().id() == ID_equal)
+        eqs.push_back(cases_it->condition());
       else
-        eqs=cases_it->guard.operands();
+        eqs = cases_it->condition().operands();
 
       // goto conversion builds disjunctions in reverse order
       // to ensure convergence, we turn this around again
@@ -839,9 +839,9 @@ bool goto_program2codet::remove_default(
     }
 
     // jumps to default are ok
-    if(it->case_last->is_goto() &&
-       it->case_last->guard.is_true() &&
-       it->case_last->get_target()==default_target)
+    if(
+      it->case_last->is_goto() && it->case_last->condition().is_true() &&
+      it->case_last->get_target() == default_target)
       continue;
 
     // fall-through is ok
@@ -860,7 +860,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
   code_blockt &dest)
 {
   // try to figure out whether this was a switch/case
-  exprt eq_cand=target->guard;
+  exprt eq_cand = target->condition();
   if(eq_cand.id()==ID_or)
     eq_cand = to_or_expr(eq_cand).op0();
 
@@ -985,7 +985,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
       {
         UNREACHABLE;
         goto_programt::instructiont i=*(it->case_selector);
-        i.guard=true_exprt();
+        i.condition_nonconst() = true_exprt();
         goto_programt tmp;
         tmp.insert_before_swap(tmp.insert_before(tmp.instructions.end()), i);
         convert_goto_goto(tmp.instructions.begin(), c);
@@ -1048,13 +1048,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
       return target;
     }
 
-    has_else=
+    has_else =
       before_else->is_goto() &&
       before_else->get_target()->location_number > end_if->location_number &&
-      before_else->guard.is_true() &&
-      (upper_bound==goto_program.instructions.end() ||
-       upper_bound->location_number>=
-       before_else->get_target()->location_number);
+      before_else->condition().is_true() &&
+      (upper_bound == goto_program.instructions.end() ||
+       upper_bound->location_number >=
+         before_else->get_target()->location_number);
 
     if(has_else)
       end_if=before_else->get_target();
@@ -1071,7 +1071,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
       return convert_goto_goto(target, dest);
   }
 
-  code_ifthenelset i(not_exprt(target->guard), code_blockt());
+  code_ifthenelset i(not_exprt(target->condition()), code_blockt());
   copy_source_location(target, i);
   simplify(i.cond(), ns);
 
@@ -1132,7 +1132,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
   if(target->get_target()==loop_end &&
      loop_last_stack.back().second)
   {
-    code_ifthenelset i(target->guard, code_continuet());
+    code_ifthenelset i(target->condition(), code_continuet());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -1156,7 +1156,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
 
   if(target->get_target()==after_loop)
   {
-    code_ifthenelset i(target->guard, code_breakt());
+    code_ifthenelset i(target->condition(), code_breakt());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -1214,7 +1214,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto(
 
   code_gotot goto_code(label.str());
 
-  code_ifthenelset i(target->guard, std::move(goto_code));
+  code_ifthenelset i(target->condition(), std::move(goto_code));
   simplify(i.cond(), ns);
 
   copy_source_location(target, i);
@@ -1281,9 +1281,12 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
   // END THREAD
   // 2: code in existing thread
   /* check the structure and compute the iterators */
-  assert(next->is_goto() && next->guard.is_true());
-  assert(!next->is_backwards_goto());
-  assert(thread_start->location_number < next->get_target()->location_number);
+  DATA_INVARIANT(
+    next->is_goto() && next->condition().is_true(), "START THREAD pattern");
+  DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern");
+  DATA_INVARIANT(
+    thread_start->location_number < next->get_target()->location_number,
+    "START THREAD pattern");
   goto_programt::const_targett after_thread_start=thread_start;
   ++after_thread_start;
 
diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp
diff --git a/src/goto-programs/ensure_one_backedge_per_target.cpp b/src/goto-programs/ensure_one_backedge_per_target.cpp
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h

Original file line number	Diff line number	Diff line change
`@@ -368,7 +368,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(`
`368`	`368`	`struct_tag_typet type(stack_catch[i][j].first);`
`369`	`369`
`370`	`370`	`java_instanceof_exprt check(exc_thrown, type);`
`371`		`- t_exc->guard=check;`
	`371`	`+ t_exc->condition_nonconst() = check;`
`372`	`372`
`373`	`373`	`if(remove_added_instanceof)`
`374`	`374`	`{`
Original file line number	Diff line number	Diff line change
`@@ -71,7 +71,7 @@ static bool is_call_to(`
`71`	`71`
`72`	`72`	`static bool is_assume_false(goto_programt::const_targett inst)`
`73`	`73`	`{`
`74`		`- return inst->is_assume() && inst->guard.is_false();`
	`74`	`+ return inst->is_assume() && inst->condition().is_false();`
`75`	`75`	`}`
`76`	`76`
`77`	`77`	/// Interpret `program`, resolving classid comparisons assuming any actual
`@@ -90,7 +90,7 @@ static goto_programt::const_targett interpret_classid_comparison(`
`90`	`90`	`{`
`91`	`91`	`if(pc->type() == GOTO)`
`92`	`92`	`{`
`93`		`- exprt guard = pc->guard;`
	`93`	`+ exprt guard = pc->condition();`
`94`	`94`	`guard = resolve_classid_test(guard, actual_class_id, ns);`
`95`	`95`	`if(guard.is_true())`
`96`	`96`	`{`
Original file line number	Diff line number	Diff line change
`@@ -92,15 +92,20 @@ SCENARIO(`
`92`	`92`	`}`
`93`	`93`	`}`
`94`	`94`
`95`		`- for(auto it = instrit->guard.depth_begin(),`
`96`		`- itend = instrit->guard.depth_end();`
`97`		`- it != itend; ++it)`
	`95`	`+ if(instrit->has_condition())`
`98`	`96`	`{`
`99`		`- if(it->id() == ID_dereference)`
	`97`	`+ const auto &condition = instrit->condition();`
	`98`	`+`
	`99`	`+ for(auto it = condition.depth_begin(),`
	`100`	`+ itend = condition.depth_end();`
	`101`	`+ it != itend;`
	`102`	`+ ++it)`
`100`	`103`	`{`
`101`		`- const auto &deref = to_dereference_expr(*it);`
`102`		`- REQUIRE(`
`103`		`- safe_pointers.is_safe_dereference(deref, instrit));`
	`104`	`+ if(it->id() == ID_dereference)`
	`105`	`+ {`
	`106`	`+ const auto &deref = to_dereference_expr(*it);`
	`107`	`+ REQUIRE(safe_pointers.is_safe_dereference(deref, instrit));`
	`108`	`+ }`
`104`	`109`	`}`
`105`	`110`	`}`
`106`	`111`	`}`
Original file line number	Diff line number	Diff line change
`@@ -71,11 +71,12 @@ SCENARIO(`
`71`	`71`	`// branching for class C and one for class D or O.`
`72`	`72`	`if(instruction.type() == goto_program_instruction_typet::GOTO)`
`73`	`73`	`{`
`74`		`- if(instruction.guard.id() == ID_equal)`
	`74`	`+ if(instruction.condition().id() == ID_equal)`
`75`	`75`	`{`
`76`	`76`	`THEN("Class C should call its specific method")`
`77`	`77`	`{`
`78`		`- const equal_exprt &eq_expr = to_equal_expr(instruction.guard);`
	`78`	`+ const equal_exprt &eq_expr =`
	`79`	`+ to_equal_expr(instruction.condition());`
`79`	`80`	`check_function_call(`
`80`	`81`	`eq_expr,`
`81`	`82`	`"java::C",`
`@@ -84,11 +85,12 @@ SCENARIO(`
`84`	`85`	`}`
`85`	`86`	`}`
`86`	`87`
`87`		`- else if(instruction.guard.id() == ID_or)`
	`88`	`+ else if(instruction.condition().id() == ID_or)`
`88`	`89`	`{`
`89`	`90`	`THEN("Classes D and O should both call O.toString()")`
`90`	`91`	`{`
`91`		`- const or_exprt &disjunction = to_or_expr(instruction.guard);`
	`92`	`+ const or_exprt &disjunction =`
	`93`	`+ to_or_expr(instruction.condition());`
`92`	`94`	`REQUIRE(`
`93`	`95`	`(disjunction.op0().id() == ID_equal &&`
`94`	`96`	`disjunction.op1().id() == ID_equal));`
Original file line number	Diff line number	Diff line change
`@@ -50,7 +50,7 @@ void instrument_intervals(`
`50`	`50`	`{`
`51`	`51`	`// we follow a branch, instrument`
`52`	`52`	`}`
`53`		`- else if(previous->is_function_call() && !previous->guard.is_true())`
	`53`	`+ else if(previous->is_function_call())`
`54`	`54`	`{`
`55`	`55`	`// we follow a function call, instrument`
`56`	`56`	`}`
Original file line number	Diff line number	Diff line change
`@@ -79,13 +79,13 @@ void variable_sensitivity_domaint::transform(`
`79`	`79`	`if(to == from->get_target())`
`80`	`80`	`{`
`81`	`81`	`// The AI is exploring the branch where the jump is taken`
`82`		`- assume(instruction.guard, ns);`
	`82`	`+ assume(instruction.condition(), ns);`
`83`	`83`	`}`
`84`	`84`	`else`
`85`	`85`	`{`
`86`	`86`	`// Exploring the path where the jump is not taken - therefore assume`
`87`	`87`	`// the condition is false`
`88`		`- assume(not_exprt(instruction.guard), ns);`
	`88`	`+ assume(not_exprt(instruction.condition()), ns);`
`89`	`89`	`}`
`90`	`90`	`}`
`91`	`91`	`// ignore jumps to the next line, we can assume nothing`
`@@ -94,7 +94,7 @@ void variable_sensitivity_domaint::transform(`
`94`	`94`	`break;`
`95`	`95`
`96`	`96`	`case ASSUME:`
`97`		`- assume(instruction.guard, ns);`
	`97`	`+ assume(instruction.condition(), ns);`
`98`	`98`	`break;`
`99`	`99`
`100`	`100`	`case FUNCTION_CALL:`
Original file line number	Diff line number	Diff line change
`@@ -258,8 +258,11 @@ int linker_script_merget::pointerize_linker_defined_symbols(`
`258`	`258`	`goto_programt &program=gf.second.body;`
`259`	`259`	`for(auto &instruction : program.instructions)`
`260`	`260`	`{`
`261`		`- for(exprt insts : std::list<exprt >(`
`262`		`- {&(instruction.code_nonconst()), &(instruction.guard)}))`
	`261`	`+ std::list<exprt *> expressions = {&instruction.code_nonconst()};`
	`262`	`+ if(instruction.has_condition())`
	`263`	`+ expressions.push_back(&instruction.condition_nonconst());`
	`264`	`+`
	`265`	`+ for(exprt *insts : expressions)`
`263`	`266`	`{`
`264`	`267`	`std::list<symbol_exprt> to_pointerize;`
`265`	`268`	`symbols_to_pointerize(linker_values, *insts, to_pointerize);`
Original file line number	Diff line number	Diff line change
`@@ -40,7 +40,7 @@ void cover_assertion_instrumentert::instrument(`
`40`	`40`	`// turn into 'assert(false)' to avoid simplification`
`41`	`41`	`if(is_non_cover_assertion(i_it))`
`42`	`42`	`{`
`43`		`- i_it->guard = false_exprt();`
	`43`	`+ i_it->condition_nonconst() = false_exprt();`
`44`	`44`	`initialize_source_location(`
`45`	`45`	`i_it, id2string(i_it->source_location().get_comment()), function_id);`
`46`	`46`	`}`