CBMC
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
17 const irep_idt &function_id,
18 goto_programt &goto_program,
20 const cover_blocks_baset &,
21 const assertion_factoryt &make_assertion) const
22{
23 if(i_it->is_assume())
24 {
25 const auto assume_condition = expr2c(i_it->condition(), ns);
26 const auto comment_before =
27 "assert(false) before assume(" + assume_condition + ")";
28 const auto comment_after =
29 "assert(false) after assume(" + assume_condition + ")";
30
31 source_locationt location = i_it->source_location();
32 initialize_source_location(location, comment_before, function_id);
33 const auto assert_before = make_assertion(false_exprt{}, location);
34 goto_program.insert_before(i_it, assert_before);
35
36 initialize_source_location(location, comment_after, function_id);
37 const auto assert_after = make_assertion(false_exprt{}, location);
38 goto_program.insert_after(i_it, assert_after);
39 }
40 // Otherwise, skip existing assertions.
41 else if(i_it->is_assert())
42 {
43 const auto location = i_it->source_location();
44 // Filter based on if assertion was added by us as part of instrumentation.
45 if(location.get_property_class() != "coverage")
46 {
47 i_it->turn_into_skip();
48 }
49 }
50}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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(source_locationt &source_location, 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:38
The Boolean constant false.
Definition std_expr.h:3199
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Coverage Instrumentation.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4155
Concrete Goto Program.
API to expression classes.