cprover
cover_instrument_decision.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 <langapi/language_util.h>
15 
16 #include "cover_util.h"
17 
19  const irep_idt &function_id,
20  goto_programt &goto_program,
22  const cover_blocks_baset &) const
23 {
24  if(is_non_cover_assertion(i_it))
25  i_it->turn_into_skip();
26 
27  // Decisions are maximal Boolean combinations of conditions.
28  if(!i_it->source_location.is_built_in())
29  {
30  const std::set<exprt> decisions = collect_decisions(i_it);
31 
32  const source_locationt source_location = i_it->source_location;
33 
34  for(const auto &d : decisions)
35  {
36  const std::string d_string = from_expr(ns, function_id, d);
37 
38  const std::string comment_t = "decision '" + d_string + "' true";
39  goto_program.insert_before_swap(i_it);
40  *i_it = goto_programt::make_assertion(d, source_location);
41  initialize_source_location(i_it, comment_t, function_id);
42 
43  const std::string comment_f = "decision '" + d_string + "' false";
44  goto_program.insert_before_swap(i_it);
45  *i_it = goto_programt::make_assertion(not_exprt(d), source_location);
46  initialize_source_location(i_it, comment_f, function_id);
47  }
48 
49  // advance iterator beyond the inserted instructions
50  for(std::size_t i = 0; i < decisions.size() * 2; i++)
51  i_it++;
52  }
53 }
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_instrumenter_baset::ns
const namespacet ns
Definition: cover_instrument.h:58
cover_decision_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_decision.cpp:18
collect_decisions
std::set< exprt > collect_decisions(const goto_programt::const_targett t)
Definition: cover_util.cpp:98
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
language_util.h
cover_instrument.h
cover_blocks_baset
Definition: cover_basic_blocks.h:24
source_locationt
Definition: source_location.h:20
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_util.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
not_exprt
Boolean negation.
Definition: std_expr.h:2872