CBMC
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 
20 class cmdlinet;
21 class goto_modelt;
23 class message_handlert;
24 class optionst;
25 class symbol_tablet;
26 
27 #define OPT_COVER \
28  "(cover):" \
29  "(cover-failed-assertions)" \
30  "(show-test-suite)"
31 
32 #define HELP_COVER \
33  " {y--cover} {uCC} \t " \
34  "create test-suite with coverage criterion {uCC}, where {uCC} is one of " \
35  "{yassertion}[{ys}], {yassume}[{ys}], {ybranch}[{yes}], " \
36  "{ycondition}[{ys}], {ycover}, {decision}[{ys}], {ylocation}[{ys}], " \
37  "or {ymcdc}\n" \
38  " {y--cover-failed-assertions} \t " \
39  "do not stop coverage checking at failed assertions (this is the default " \
40  "for {y--cover} {yassertions})\n" \
41  " {y--show-test-suite} \t " \
42  "print test suite for coverage criterion (requires {y--cover})\n"
43 
45 {
46  ASSUME,
47  LOCATION,
48  BRANCH,
49  DECISION,
50  CONDITION,
51  PATH,
52  MCDC,
53  ASSERTION,
54  COVER // __CPROVER_cover(x) annotations
55 };
56 
58 {
64  // cover instruments point to goal_filters, so they must be stored on the heap
65  std::unique_ptr<goal_filterst> goal_filters =
66  std::make_unique<goal_filterst>();
70 };
71 
73  const symbol_tablet &,
74  const cover_configt &,
77  message_handlert &message_handler);
78 
80  const symbol_tablet &,
81  const cover_configt &,
82  goto_programt &,
84  message_handlert &message_handler);
85 
88 
90  const optionst &,
91  const irep_idt &main_function_id,
92  const symbol_tablet &,
94 
96  const cover_configt &,
99 
100 void parse_cover_options(const cmdlinet &, optionst &);
101 
103  const cover_configt &,
104  const symbol_tablet &,
105  goto_functionst &,
106  message_handlert &);
107 
109  const cover_configt &,
110  goto_modelt &,
111  message_handlert &);
112 
113 #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:38
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:64
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.
Definition: goto_program.h:73
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
The symbol table.
Definition: symbol_table.h:14
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
Definition: cover.cpp:143
coverage_criteriont
Definition: cover.h:45
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:181
Filters for the Coverage Instrumentation.
Coverage Instrumentation.
bool traces_must_terminate
Definition: cover.h:61
irep_idt mode
Definition: cover.h:62
bool keep_assertions
Definition: cover.h:59
cover_instrumenterst cover_instrumenters
Definition: cover.h:67
bool cover_failed_assertions
Definition: cover.h:60
cover_instrumenter_baset::assertion_factoryt make_assertion
Definition: cover.h:68
function_filterst function_filters
Definition: cover.h:63
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:65