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  goto_programt &goto_program,
20  const cover_blocks_baset &basic_blocks) const
21 {
22  if(is_non_cover_assertion(i_it))
23  i_it->make_skip();
24 
25  const std::size_t block_nr = basic_blocks.block_of(i_it);
26  const auto representative_instruction = basic_blocks.instruction_of(block_nr);
27  // we only instrument the selected instruction
28  if(representative_instruction && *representative_instruction == i_it)
29  {
30  const std::string b = std::to_string(block_nr + 1); // start with 1
31  const std::string id = id2string(i_it->function) + "#" + b;
32  const auto source_location = basic_blocks.source_location_of(block_nr);
33 
34  // filter goals
35  if(goal_filters(source_location))
36  {
37  const std::string comment = "block " + b;
38  const irep_idt function = i_it->function;
39  goto_program.insert_before_swap(i_it);
40  i_it->make_assertion(false_exprt());
41  i_it->source_location = source_location;
42  initialize_source_location(i_it, comment, function);
43  i_it++;
44  }
45  }
46 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Coverage Instrumentation.
Basic blocks detection for Coverage Instrumentation.
virtual optionalt< goto_programt::const_targett > instruction_of(std::size_t block_nr) const =0
instructionst::iterator targett
Definition: goto_program.h:414
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual std::size_t block_of(goto_programt::const_targett t) const =0
The Boolean constant false.
Definition: std_expr.h:4452
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
const goal_filterst & goal_filters
Filters for the Coverage Instrumentation.
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function) const
bool is_non_cover_assertion(goto_programt::const_targett t) const
virtual const source_locationt & source_location_of(std::size_t block_nr) const =0