cprover
cover_instrument_assume.cpp
Go to the documentation of this file.
1 
5 #include "cover_instrument.h"
6 
7 #include "ansi-c/expr2c.h"
9 #include "util/std_expr.h"
10 #include <util/namespace.h>
11 
18  const irep_idt &function_id,
19  goto_programt &goto_program,
21  const cover_blocks_baset &,
22  const assertion_factoryt &make_assertion) const
23 {
24  if(i_it->is_assume())
25  {
26  const auto location = i_it->source_location();
27  const auto assume_condition =
28  expr2c(i_it->get_condition(), namespacet{symbol_tablet()});
29  const auto comment_before =
30  "assert(false) before assume(" + assume_condition + ")";
31  const auto comment_after =
32  "assert(false) after assume(" + assume_condition + ")";
33 
34  const auto assert_before = make_assertion(false_exprt{}, location);
35  goto_programt::targett t = goto_program.insert_before(i_it, assert_before);
36  initialize_source_location(t, comment_before, function_id);
37 
38  const auto assert_after = make_assertion(false_exprt{}, location);
39  t = goto_program.insert_after(i_it, assert_after);
40  initialize_source_location(t, comment_after, function_id);
41  }
42  // Otherwise, skip existing assertions.
43  else if(i_it->is_assert())
44  {
45  const auto location = i_it->source_location();
46  // Filter based on if assertion was added by us as part of instrumentation.
47  if(location.get_property_class() != "coverage")
48  {
49  i_it->turn_into_skip();
50  }
51  }
52 }
void instrument(const irep_idt &, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Instrument program to check coverage of assume statements.
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The Boolean constant false.
Definition: std_expr.h:2865
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Coverage Instrumentation.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
Concrete Goto Program.
API to expression classes.