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 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 {
43  // cover instruments point to goal_filters, so they must be stored on the heap
44  std::unique_ptr<goal_filterst> goal_filters =
45  util_make_unique<goal_filterst>();
47 };
48 
50  const symbol_tablet &,
51  const cover_configt &,
54  message_handlert &message_handler);
55 
57  const symbol_tablet &,
58  const cover_configt &,
59  goto_programt &,
61  message_handlert &message_handler);
62 
65 
67  const optionst &,
68  const irep_idt &main_function_id,
69  const symbol_tablet &,
71 
73  const cover_configt &,
76 
77 void parse_cover_options(const cmdlinet &, optionst &);
78 
80  const cover_configt &,
81  const symbol_tablet &,
84 
86  const cover_configt &,
87  goto_modelt &,
89 
90 #endif // CPROVER_GOTO_INSTRUMENT_COVER_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
get_cover_config
cover_configt get_cover_config(const optionst &, const symbol_tablet &, message_handlert &)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:171
coverage_criteriont::COVER
@ COVER
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
cover_configt::goal_filters
std::unique_ptr< goal_filterst > goal_filters
Definition: cover.h:44
optionst
Definition: options.h:23
parse_cover_options
void parse_cover_options(const cmdlinet &, optionst &)
Parses coverage-related command line options.
Definition: cover.cpp:137
coverage_criteriont::PATH
@ PATH
goto_modelt
Definition: goto_model.h:26
coverage_criteriont
coverage_criteriont
Definition: cover.h:26
cover_configt::mode
irep_idt mode
Definition: cover.h:41
coverage_criteriont::ASSERTION
@ ASSERTION
coverage_criteriont::CONDITION
@ CONDITION
coverage_criteriont::LOCATION
@ LOCATION
cover_configt::cover_instrumenters
cover_instrumenterst cover_instrumenters
Definition: cover.h:46
cmdlinet
Definition: cmdline.h:21
instrument_cover_goals
void instrument_cover_goals(const symbol_tablet &, const cover_configt &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
make_unique.h
coverage_criteriont::DECISION
@ DECISION
cover_configt::traces_must_terminate
bool traces_must_terminate
Definition: cover.h:40
cover_instrument.h
message_handlert
Definition: message.h:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
cover_configt::function_filters
function_filterst function_filters
Definition: cover.h:42
coverage_criteriont::BRANCH
@ BRANCH
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
coverage_criteriont::MCDC
@ MCDC
cover_configt
Definition: cover.h:38
function_filterst
A collection of function filters to be applied in conjunction.
Definition: cover_filter.h:76
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
cover_filter.h
cover_configt::keep_assertions
bool keep_assertions
Definition: cover.h:39
cover_instrumenterst
A collection of instrumenters to be run.
Definition: cover_instrument.h:88