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;
26class symbol_tablet;
27
28#define OPT_COVER \
29 "(cover):" \
30 "(cover-failed-assertions)" \
31 "(show-test-suite)"
32
33#define HELP_COVER \
34 " {y--cover} {uCC} \t " \
35 "create test-suite with coverage criterion {uCC}, where {uCC} is one of " \
36 "{yassertion}[{ys}], {yassume}[{ys}], {ybranch}[{yes}], " \
37 "{ycondition}[{ys}], {ycover}, {decision}[{ys}], {ylocation}[{ys}], " \
38 "or {ymcdc}\n" \
39 " {y--cover-failed-assertions} \t " \
40 "do not stop coverage checking at failed assertions (this is the default " \
41 "for {y--cover} {yassertions})\n" \
42 " {y--show-test-suite} \t " \
43 "print test suite for coverage criterion (requires {y--cover})\n"
44
46{
47 ASSUME,
49 BRANCH,
52 PATH,
53 MCDC,
55 COVER // __CPROVER_cover(x) annotations
56};
57
72
74 const symbol_tablet &,
75 const cover_configt &,
78 message_handlert &message_handler);
79
81 const symbol_tablet &,
82 const cover_configt &,
85 message_handlert &message_handler);
86
89
91 const optionst &,
93 const symbol_tablet &,
95
97 const cover_configt &,
100
101void parse_cover_options(const cmdlinet &, optionst &);
102
104 const cover_configt &,
105 const symbol_tablet &,
108
110 const cover_configt &,
111 goto_modelt &,
113
114#endif // CPROVER_GOTO_INSTRUMENT_COVER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
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:190
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:46
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:62
irep_idt mode
Definition cover.h:63
bool keep_assertions
Definition cover.h:60
cover_instrumenterst cover_instrumenters
Definition cover.h:68
bool cover_failed_assertions
Definition cover.h:61
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition cover.h:69
function_filterst function_filters
Definition cover.h:64
std::unique_ptr< goal_filterst > goal_filters
Definition cover.h:66