cprover
cover.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 Date: 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 
21 class cmdlinet;
22 class goto_modelt;
24 class message_handlert;
25 class 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,
45  LOCATION,
46  BRANCH,
47  DECISION,
48  CONDITION,
49  PATH,
50  MCDC,
51  ASSERTION,
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 &,
80  goto_programt &,
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 
98 void parse_cover_options(const cmdlinet &, optionst &);
99 
101  const cover_configt &,
102  const symbol_tablet &,
103  goto_functionst &,
104  message_handlert &);
105 
107  const cover_configt &,
108  goto_modelt &,
109  message_handlert &);
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.
Definition: cover_filter.h:62
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.
Definition: goto_program.h:73
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
The symbol table.
Definition: symbol_table.h:14
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