cprover
cover_instrument_location.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: 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,
21  const cover_blocks_baset &basic_blocks) const
22 {
23  if(is_non_cover_assertion(i_it))
24  i_it->turn_into_skip();
25 
26  const std::size_t block_nr = basic_blocks.block_of(i_it);
27  const auto representative_instruction = basic_blocks.instruction_of(block_nr);
28  // we only instrument the selected instruction
29  if(representative_instruction && *representative_instruction == i_it)
30  {
31  const std::string b = std::to_string(block_nr + 1); // start with 1
32  const std::string id = id2string(function_id) + "#" + b;
33  const auto source_location = basic_blocks.source_location_of(block_nr);
34 
35  // filter goals
36  if(goal_filters(source_location))
37  {
38  const std::string source_lines =
39  id2string(source_location.get_basic_block_source_lines());
40  const std::string comment =
41  "block " + b + " (lines " + source_lines + ")";
42  goto_program.insert_before_swap(i_it);
43  *i_it = goto_programt::make_assertion(false_exprt(), source_location);
44  initialize_source_location(i_it, comment, function_id);
45  i_it++;
46  }
47  }
48 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cover_instrumenter_baset::is_non_cover_assertion
bool is_non_cover_assertion(goto_programt::const_targett t) const
Definition: cover_instrument.h:79
cover_instrumenter_baset::initialize_source_location
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
Definition: cover_instrument.h:68
cover_blocks_baset::source_location_of
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
cover_instrumenter_baset::goal_filters
const goal_filterst & goal_filters
Definition: cover_instrument.h:59
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cover_instrument.h
cover_blocks_baset::instruction_of
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
cover_blocks_baset
Definition: cover_basic_blocks.h:24
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
cover_location_instrumentert::instrument
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_location.cpp:17
cover_basic_blocks.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
cover_blocks_baset::block_of
virtual std::size_t block_of(goto_programt::const_targett t) const =0
cover_filter.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579