cprover
cover_instrument_branch.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_basic_blocks.h"
13 #include "cover_filter.h"
14 #include "cover_instrument.h"
15 
17  const irep_idt &function_id,
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->turn_into_skip();
24 
25  const bool is_function_entry_point =
26  i_it == goto_program.instructions.begin();
27  const bool is_conditional_goto = i_it->is_goto() && !i_it->guard.is_true();
28  if(!is_function_entry_point && !is_conditional_goto)
29  return;
30 
31  if(!goal_filters(i_it->source_location))
32  return;
33 
34  if(is_function_entry_point)
35  {
36  // we want branch coverage to imply 'entry point of function'
37  // coverage
38  std::string comment = "entry point";
39 
40  source_locationt source_location = i_it->source_location;
41 
42  goto_programt::targett t = goto_program.insert_before(
43  i_it, goto_programt::make_assertion(false_exprt(), source_location));
44  initialize_source_location(t, comment, function_id);
45  }
46 
47  if(is_conditional_goto)
48  {
49  std::string b =
50  std::to_string(basic_blocks.block_of(i_it) + 1); // start with 1
51  std::string true_comment = "block " + b + " branch true";
52  std::string false_comment = "block " + b + " branch false";
53 
54  exprt guard = i_it->guard;
55  source_locationt source_location = i_it->source_location;
56 
57  goto_program.insert_before_swap(i_it);
58  *i_it = goto_programt::make_assertion(not_exprt(guard), source_location);
59  initialize_source_location(i_it, true_comment, function_id);
60 
61  goto_program.insert_before_swap(i_it);
62  *i_it = goto_programt::make_assertion(guard, source_location);
63  initialize_source_location(i_it, false_comment, function_id);
64 
65  std::advance(i_it, 2);
66  }
67 }
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
exprt
Base class for all expressions.
Definition: expr.h:53
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::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
cover_instrument.h
cover_blocks_baset
Definition: cover_basic_blocks.h:24
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
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
cover_branch_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_branch.cpp:16
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
not_exprt
Boolean negation.
Definition: std_expr.h:2872