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 
18 #include "cover_filter.h"
19 #include "cover_instrument.h"
20 
21 class message_handlert;
22 class cmdlinet;
23 class optionst;
24 
26 {
27  LOCATION,
28  BRANCH,
29  DECISION,
30  CONDITION,
31  PATH,
32  MCDC,
33  ASSERTION,
34  COVER // __CPROVER_cover(x) annotations
35 };
36 
38 {
45 };
46 
48  const symbol_tablet &,
52 
54  const symbol_tablet &,
55  goto_programt &,
58 
59 std::unique_ptr<cover_configt> get_cover_config(
60  const optionst &, const symbol_tablet &, message_handlert &);
61 
63  const cover_configt &,
66 
67 void parse_cover_options(const cmdlinet &, optionst &);
68 
70  const optionst &,
71  const symbol_tablet &,
74 
76  const optionst &,
77  goto_modelt &,
79 
80 #endif // CPROVER_GOTO_INSTRUMENT_COVER_H
coverage_criteriont
Definition: cover.h:25
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:74
void instrument_cover_goals(const symbol_tablet &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
Coverage Instrumentation.
Symbol Table + CFG.
bool keep_assertions
Definition: cover.h:39
bool traces_must_terminate
Definition: cover.h:40
The symbol table.
Definition: symbol_table.h:19
irep_idt mode
Definition: cover.h:41
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
Definition: cover.cpp:163
std::unique_ptr< cover_configt > get_cover_config(const optionst &, const symbol_tablet &, message_handlert &)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:187
Filters for the Coverage Instrumentation.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
cover_instrumenterst cover_instrumenters
Definition: cover.h:44
A collection of instrumenters to be run.
function_filterst function_filters
Definition: cover.h:42
goal_filterst goal_filters
Definition: cover.h:43
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147