cprover
Loading...
Searching...
No Matches
symex_coverage.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Record and print code coverage of symbolic execution
4
5Author: Michael Tautschnig
6
7Date: 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
24class goto_functionst;
25class namespacet;
26class xmlt;
27
29{
30public:
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
49protected:
50 const namespacet &ns;
51
53 {
57 unsigned _num_executions)
58 : location(_from), num_executions(_num_executions), succ(_to)
59 {
60 }
61
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
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)