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_instrument.h"
13 #include "cover_basic_blocks.h"
14 
16  goto_programt &goto_program,
18  const cover_blocks_baset &basic_blocks) const
19 {
20  if(is_non_cover_assertion(i_it))
21  i_it->make_skip();
22 
23  if(i_it == goto_program.instructions.begin())
24  {
25  // we want branch coverage to imply 'entry point of function'
26  // coverage
27  std::string comment = "entry point";
28 
29  source_locationt source_location = i_it->source_location;
30 
31  goto_programt::targett t = goto_program.insert_before(i_it);
32  t->make_assertion(false_exprt());
33  t->source_location = source_location;
34  initialize_source_location(t, comment, i_it->function);
35  }
36 
37  if(
38  i_it->is_goto() && !i_it->guard.is_true() &&
39  !i_it->source_location.is_built_in())
40  {
41  std::string b =
42  std::to_string(basic_blocks.block_of(i_it) + 1); // start with 1
43  std::string true_comment = "block " + b + " branch true";
44  std::string false_comment = "block " + b + " branch false";
45 
46  exprt guard = i_it->guard;
47  const irep_idt function = i_it->function;
48  source_locationt source_location = i_it->source_location;
49 
50  goto_program.insert_before_swap(i_it);
51  i_it->make_assertion(not_exprt(guard));
52  i_it->source_location = source_location;
53  initialize_source_location(i_it, true_comment, function);
54 
55  goto_program.insert_before_swap(i_it);
56  i_it->make_assertion(guard);
57  i_it->source_location = source_location;
58  initialize_source_location(i_it, false_comment, function);
59 
60  std::advance(i_it, 2);
61  }
62 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
cover_instrumenter_baset::is_non_cover_assertion
bool is_non_cover_assertion(goto_programt::const_targett t) const
Definition: cover_instrument.h:77
cover_branch_instrumentert::instrument
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Definition: cover_instrument_branch.cpp:15
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
exprt
Base class for all expressions.
Definition: expr.h:54
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
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:510
cover_instrument.h
cover_blocks_baset
Definition: cover_basic_blocks.h:21
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
cover_instrumenter_baset::initialize_source_location
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function) const
Definition: cover_instrument.h:65
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
cover_basic_blocks.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
cover_blocks_baset::block_of
virtual std::size_t block_of(goto_programt::const_targett t) const =0
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
not_exprt
Boolean negation.
Definition: std_expr.h:3308