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 <
goto-programs/goto_model.h
>
18
#include <
util/cmdline.h
>
19
20
class
message_handlert
;
21
22
enum class
coverage_criteriont
23
{
24
LOCATION
,
BRANCH
,
DECISION
,
CONDITION
,
25
PATH
,
MCDC
,
ASSERTION
,
COVER
};
26
27
void
instrument_cover_goals
(
28
const
symbol_tablet
&symbol_table,
29
goto_programt
&goto_program,
30
coverage_criteriont
);
31
32
void
instrument_cover_goals
(
33
const
symbol_tablet
&symbol_table,
34
goto_functionst
&goto_functions,
35
coverage_criteriont
);
36
37
bool
instrument_cover_goals
(
38
const
cmdlinet
&cmdline,
39
const
symbol_tablet
&symbol_table,
40
goto_functionst
&goto_functions,
41
message_handlert
&msgh);
42
43
#endif // CPROVER_GOTO_INSTRUMENT_COVER_H
coverage_criteriont
coverage_criteriont
Definition:
cover.h:22
coverage_criteriont::BRANCH
coverage_criteriont::CONDITION
coverage_criteriont::MCDC
coverage_criteriont::LOCATION
instrument_cover_goals
void instrument_cover_goals(const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont)
Definition:
cover.cpp:832
coverage_criteriont::PATH
cmdlinet
Definition:
cmdline.h:17
goto_model.h
Symbol Table + CFG.
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
coverage_criteriont::COVER
message_handlert
Definition:
message.h:20
goto_functionst
Definition:
goto_functions.h:20
coverage_criteriont::ASSERTION
goto_programt
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition:
goto_program.h:24
coverage_criteriont::DECISION
cmdline.h
goto-instrument
cover.h
Generated by
1.8.12