cprover
Loading...
Searching...
No Matches
cover_instrument_assume.cpp
Go to the documentation of this file.
1
4
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.