cprover
Loading...
Searching...
No Matches
cover_instrument_location.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "cover_instrument.h"
13
14#include "cover_basic_blocks.h"
15#include "cover_filter.h"
16
18 const irep_idt &function_id,
19 goto_programt &goto_program,
22 const assertion_factoryt &make_assertion) const
23{
25 i_it->turn_into_skip();
26
27 const std::size_t block_nr = basic_blocks.block_of(i_it);
28 const auto representative_instruction = basic_blocks.instruction_of(block_nr);
29 // we only instrument the selected instruction
31 {
32 const std::string b = std::to_string(block_nr + 1); // start with 1
33 const std::string id = id2string(function_id) + "#" + b;
34 const auto source_location = basic_blocks.source_location_of(block_nr);
35
36 // filter goals
37 if(goal_filters(source_location))
38 {
39 const std::string source_lines =
40 id2string(source_location.get_basic_block_source_lines());
41 const std::string comment =
42 "block " + b + " (lines " + source_lines + ")";
43 goto_program.insert_before_swap(i_it);
44 *i_it = make_assertion(false_exprt(), source_location);
46 i_it++;
47 }
48 }
49}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
const goal_filterst & goal_filters
bool is_non_cover_assertion(goto_programt::const_targett t) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
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.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
Basic blocks detection for Coverage Instrumentation.
Filters for the Coverage Instrumentation.
Coverage Instrumentation.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static std::string comment(const rw_set_baset::entryt &entry, bool write)