cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
cover_filter.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Coverage Instrumentation
4
5
Author: Peter Schrammel
6
7
\*******************************************************************/
8
11
12
#include "
cover_filter.h
"
13
14
#include <
util/prefix.h
>
15
#include <
util/symbol.h
>
16
17
#include <
linking/static_lifetime_init.h
>
18
23
bool
internal_functions_filtert::operator()
(
24
const
symbolt
&function,
25
const
goto_functionst::goto_functiont
&goto_function)
const
26
{
27
if
(function.
name
==
goto_functionst::entry_point
())
28
return
false
;
29
30
if
(function.
name
==
INITIALIZE_FUNCTION
)
31
return
false
;
32
33
if
(goto_function.is_hidden())
34
return
false
;
35
36
// ignore Java built-ins (synthetic functions)
37
if
(function.
name
.
starts_with
(
"java::array["
))
38
return
false
;
39
40
// ignore if built-in library
41
if
(
42
!goto_function.body.instructions.empty() &&
43
goto_function.body.instructions.front().source_location().is_built_in())
44
return
false
;
45
46
return
true
;
47
}
48
55
bool
file_filtert::operator()
(
56
const
symbolt
&function,
57
const
goto_functionst::goto_functiont
&goto_function)
const
58
{
59
(void)goto_function;
// unused parameter
60
return
function.
location
.
get_file
() ==
file_id
;
61
}
62
69
bool
single_function_filtert::operator()
(
70
const
symbolt
&function,
71
const
goto_functionst::goto_functiont
&goto_function)
const
72
{
73
(void)goto_function;
// unused parameter
74
return
function.
name
==
function_id
;
75
}
76
81
bool
include_pattern_filtert::operator()
(
82
const
symbolt
&function,
83
const
goto_functionst::goto_functiont
&goto_function)
const
84
{
85
(void)goto_function;
// unused parameter
86
std::smatch string_matcher;
87
return
std::regex_match(
88
id2string
(function.
name
), string_matcher,
regex_matcher
);
89
}
90
100
bool
trivial_functions_filtert::operator()
(
101
const
symbolt
&function,
102
const
goto_functionst::goto_functiont
&goto_function)
const
103
{
104
(void)function;
// unused parameter
105
unsigned
long
count_assignments = 0, count_goto = 0;
106
for
(
const
auto
&instruction : goto_function.body.instructions)
107
{
108
if
(instruction.is_goto())
109
{
110
if
((++count_goto) >= 2)
111
return
true
;
112
}
113
else
if
(instruction.is_assign())
114
{
115
if
((++count_assignments) >= 5)
116
return
true
;
117
}
118
else
if
(instruction.is_decl())
119
return
true
;
120
}
121
122
return
false
;
123
}
124
128
bool
internal_goals_filtert::
129
operator()
(
const
source_locationt
&source_location)
const
130
{
131
if
(source_location.
get_file
().
empty
())
132
return
false
;
133
134
if
(source_location.
is_built_in
())
135
return
false
;
136
137
return
true
;
138
}
dstringt::starts_with
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition
dstring.h:95
dstringt::empty
bool empty() const
Definition
dstring.h:89
file_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out all functions except those defined in the file that is given in the constructor.
Definition
cover_filter.cpp:55
file_filtert::file_id
irep_idt file_id
Definition
cover_filter.h:154
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition
goto_functions.h:27
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition
goto_functions.h:97
include_pattern_filtert::regex_matcher
std::regex regex_matcher
Definition
cover_filter.h:187
include_pattern_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name matches the regex.
Definition
cover_filter.cpp:81
internal_functions_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out functions that are not considered provided by the user.
Definition
cover_filter.cpp:23
internal_goals_filtert::operator()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Definition
cover_filter.cpp:129
single_function_filtert::function_id
irep_idt function_id
Definition
cover_filter.h:170
single_function_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out all functions except for one particular function given in the constructor.
Definition
cover_filter.cpp:69
source_locationt
Definition
source_location.h:20
source_locationt::get_file
const irep_idt & get_file() const
Definition
source_location.h:36
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition
source_location.cpp:16
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition
symbol.h:37
symbolt::name
irep_idt name
The unique identifier.
Definition
symbol.h:40
trivial_functions_filtert::operator()
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Definition
cover_filter.cpp:100
cover_filter.h
Filters for the Coverage Instrumentation.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
prefix.h
static_lifetime_init.h
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition
static_lifetime_init.h:24
symbol.h
Symbol table entry.
goto-instrument
cover_filter.cpp
Generated by
1.17.0