cprover
symex_coverage.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Record and print code coverage of symbolic execution
4 
5 Author: Michael Tautschnig
6 
7 Date: March 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_CBMC_SYMEX_COVERAGE_H
15 #define CPROVER_CBMC_SYMEX_COVERAGE_H
16 
17 #include <iosfwd>
18 #include <map>
19 #include <string>
20 
22 
23 class coverage_recordt;
24 class goto_functionst;
25 class namespacet;
26 class xmlt;
27 
29 {
30 public:
31  explicit symex_coveraget(const namespacet &_ns) : ns(_ns)
32  {
33  }
34 
35  void
37  {
38  std::pair<coverage_innert::iterator, bool> entry =
39  coverage[from].insert({to, coverage_infot(from, to, 1)});
40 
41  if(!entry.second)
42  ++(entry.first->second.num_executions);
43  }
44 
45  bool generate_report(
46  const goto_functionst &goto_functions,
47  const std::string &path) const;
48 
49 protected:
50  const namespacet &ns;
51 
53  {
57  unsigned _num_executions)
58  : location(_from), num_executions(_num_executions), succ(_to)
59  {
60  }
61 
63  unsigned num_executions;
65  };
66 
67  typedef std::map<goto_programt::const_targett, coverage_infot>
69  typedef std::map<goto_programt::const_targett, coverage_innert> coveraget;
71 
72  bool
73  output_report(const goto_functionst &goto_functions, std::ostream &os) const;
74 
75  void build_cobertura(
76  const goto_functionst &goto_functions,
77  xmlt &xml_coverage) const;
78 
80  const goto_functionst &goto_functions,
81  coverage_recordt &dest) const;
82 
84 };
85 
86 #endif // CPROVER_CBMC_SYMEX_COVERAGE_H
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:551
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
symex_coveraget(const namespacet &_ns)
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
std::map< goto_programt::const_targett, coverage_infot > coverage_innert
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
std::map< goto_programt::const_targett, coverage_innert > coveraget
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
const namespacet & ns
coveraget coverage
Definition: xml.h:21
Concrete Goto Program.
goto_programt::const_targett location
goto_programt::const_targett succ
coverage_infot(goto_programt::const_targett _from, goto_programt::const_targett _to, unsigned _num_executions)