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 <string>
18 #include <ostream>
19 #include <map>
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
coveraget coverage
void build_cobertura(const goto_functionst &goto_functions, xmlt &xml_coverage) const
coverage_infot(goto_programt::const_targett _from, goto_programt::const_targett _to, unsigned _num_executions)
symex_coveraget(const namespacet &_ns)
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
std::map< goto_programt::const_targett, coverage_innert > coveraget
goto_programt::const_targett location
void compute_overall_coverage(const goto_functionst &goto_functions, coverage_recordt &dest) const
instructionst::const_iterator const_targett
bool output_report(const goto_functionst &goto_functions, std::ostream &os) const
std::map< goto_programt::const_targett, coverage_infot > coverage_innert
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
const namespacet & ns
goto_programt::const_targett succ
Concrete Goto Program.