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 covered(
38  {
39  std::pair<coverage_innert::iterator, bool> entry=
40  coverage[from].insert({to, coverage_infot(from, to, 1)});
41 
42  if(!entry.second)
43  ++(entry.first->second.num_executions);
44  }
45 
46  bool generate_report(
47  const goto_functionst &goto_functions,
48  const std::string &path) const;
49 
50 protected:
51  const namespacet &ns;
52 
54  {
58  unsigned _num_executions):
59  location(_from), num_executions(_num_executions),
60  succ(_to)
61  {
62  }
63 
65  unsigned num_executions;
67  };
68 
69  typedef std::map<goto_programt::const_targett, coverage_infot>
71  typedef std::map<goto_programt::const_targett, coverage_innert>
74 
75  bool output_report(
76  const goto_functionst &goto_functions,
77  std::ostream &os) const;
78 
79  void build_cobertura(
80  const goto_functionst &goto_functions,
81  xmlt &xml_coverage) const;
82 
84  const goto_functionst &goto_functions,
85  coverage_recordt &dest) const;
86 
88 };
89 
90 #endif // CPROVER_CBMC_SYMEX_COVERAGE_H
symex_coveraget::compute_overall_coverage
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
Definition: symex_coverage.cpp:310
symex_coveraget
Definition: symex_coverage.h:28
symex_coveraget::coverage_innert
std::map< goto_programt::const_targett, coverage_infot > coverage_innert
Definition: symex_coverage.h:70
symex_coveraget::coveraget
std::map< goto_programt::const_targett, coverage_innert > coveraget
Definition: symex_coverage.h:72
symex_coveraget::build_cobertura
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
Definition: symex_coverage.cpp:386
symex_coveraget::coverage
coveraget coverage
Definition: symex_coverage.h:73
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
symex_coveraget::symex_coveraget
symex_coveraget(const namespacet &_ns)
Definition: symex_coverage.h:31
symex_coveraget::output_report
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
Definition: symex_coverage.cpp:431
symex_coveraget::generate_report
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_coverage.cpp:446
symex_coveraget::coverage_infot::location
goto_programt::const_targett location
Definition: symex_coverage.h:64
symex_coveraget::covered
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
Definition: symex_coverage.h:35
symex_coveraget::coverage_infot::coverage_infot
coverage_infot(goto_programt::const_targett _from, goto_programt::const_targett _to, unsigned _num_executions)
Definition: symex_coverage.h:55
xmlt
Definition: xml.h:18
goto_program.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
symex_coveraget::ns
const namespacet & ns
Definition: symex_coverage.h:51
symex_coveraget::coverage_infot
Definition: symex_coverage.h:53
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
symex_coveraget::coverage_infot::num_executions
unsigned num_executions
Definition: symex_coverage.h:65
coverage_recordt
Definition: symex_coverage.cpp:31
goto_program_coverage_recordt
Definition: symex_coverage.cpp:50
symex_coveraget::coverage_infot::succ
goto_programt::const_targett succ
Definition: symex_coverage.h:66