cprover
Loading...
Searching...
No Matches
cover.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7Date: May 2016
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
15#define CPROVER_GOTO_INSTRUMENT_COVER_H
16
17#include "cover_filter.h"
18#include "cover_instrument.h"
19#include "util/make_unique.h"
20
21class cmdlinet;
22class goto_modelt;
25class optionst;
26
27#define OPT_COVER \
28 "(cover):" \
29 "(cover-failed-assertions)" \
30 "(show-test-suite)"
31
32#define HELP_COVER \
33 " --cover CC create test-suite with coverage criterion " \
34 "CC\n" \
35 " --cover-failed-assertions do not stop coverage checking at failed " \
36 "assertions\n" \
37 " (this is the default for --cover " \
38 "assertions)\n" \
39 " --show-test-suite print test suite for coverage criterion " \
40 "(requires --cover)\n"
41
43{
44 ASSUME,
46 BRANCH,
49 PATH,
50 MCDC,
52 COVER // __CPROVER_cover(x) annotations
53};
54
56{
62 // cover instruments point to goal_filters, so they must be stored on the heap
63 std::unique_ptr<goal_filterst> goal_filters =
64 util_make_unique<goal_filterst>();
68};
69
71 const symbol_tablet &,
72 const cover_configt &,
75 message_handlert &message_handler);
76
78 const symbol_tablet &,
79 const cover_configt &,
82 message_handlert &message_handler);
83
86
88 const optionst &,
89 const irep_idt &main_function_id,
90 const symbol_tablet &,
92
94 const cover_configt &,
97
99
101 const cover_configt &,
102 const symbol_tablet &,
105
107 const cover_configt &,
108 goto_modelt &,
110
111#endif // CPROVER_GOTO_INSTRUMENT_COVER_H
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
A collection of instrumenters to be run.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
A collection of function filters to be applied in conjunction.
A collection of goto functions.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:183
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
The symbol table.
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
Definition cover.cpp:148
coverage_criteriont
Definition cover.h:43
void instrument_cover_goals(const symbol_tablet &, const cover_configt &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
cover_configt get_cover_config(const optionst &, const symbol_tablet &, message_handlert &)
Build data structures controlling coverage from command-line options.
Definition cover.cpp:186
Filters for the Coverage Instrumentation.
Coverage Instrumentation.
bool traces_must_terminate
Definition cover.h:59
irep_idt mode
Definition cover.h:60
bool keep_assertions
Definition cover.h:57
cover_instrumenterst cover_instrumenters
Definition cover.h:65
bool cover_failed_assertions
Definition cover.h:58
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition cover.h:66
function_filterst function_filters
Definition cover.h:61
std::unique_ptr< goal_filterst > goal_filters
Definition cover.h:63