cprover
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 
17 
23  const symbolt &function,
24  const goto_functionst::goto_functiont &goto_function) const
25 {
26  if(function.name == goto_functionst::entry_point())
27  return false;
28 
29  if(function.name == INITIALIZE_FUNCTION)
30  return false;
31 
32  if(function.is_hidden())
33  return false;
34 
35  // ignore Java built-ins (synthetic functions)
36  if(has_prefix(id2string(function.name), "java::array["))
37  return false;
38 
39  // ignore if built-in library
40  if(
41  !goto_function.body.instructions.empty() &&
42  goto_function.body.instructions.front().source_location.is_built_in())
43  return false;
44 
45  return true;
46 }
47 
55  const symbolt &function,
56  const goto_functionst::goto_functiont &goto_function) const
57 {
58  (void)goto_function; // unused parameter
59  return function.location.get_file() == file_id;
60 }
61 
69  const symbolt &function,
70  const goto_functionst::goto_functiont &goto_function) const
71 {
72  (void)goto_function; // unused parameter
73  return function.name == function_id;
74 }
75 
81  const symbolt &function,
82  const goto_functionst::goto_functiont &goto_function) const
83 {
84  (void)goto_function; // unused parameter
85  std::smatch string_matcher;
86  return std::regex_match(
87  id2string(function.name), string_matcher, regex_matcher);
88 }
89 
100  const symbolt &function,
101  const goto_functionst::goto_functiont &goto_function) const
102 {
103  (void)function; // unused parameter
104  unsigned long count_assignments = 0, count_goto = 0;
105  forall_goto_program_instructions(i_it, goto_function.body)
106  {
107  if(i_it->is_goto())
108  {
109  if((++count_goto) >= 2)
110  return true;
111  }
112  else if(i_it->is_assign())
113  {
114  if((++count_assignments) >= 5)
115  return true;
116  }
117  else if(i_it->is_decl())
118  return true;
119  }
120 
121  return false;
122 }
123 
128 operator()(const source_locationt &source_location) const
129 {
130  if(source_location.get_file().empty())
131  return false;
132 
133  if(source_location.is_built_in())
134  return false;
135 
136  return true;
137 }
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:68
include_pattern_filtert::regex_matcher
std::regex regex_matcher
Definition: cover_filter.h:212
prefix.h
single_function_filtert::function_id
irep_idt function_id
Definition: cover_filter.h:192
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:99
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:54
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
dstringt::empty
bool empty() const
Definition: dstring.h:88
source_locationt
Definition: source_location.h:20
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
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:80
file_filtert::file_id
irep_idt file_id
Definition: cover_filter.h:174
symbolt
Symbol table entry.
Definition: symbol.h:28
internal_goals_filtert::operator()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Definition: cover_filter.cpp:128
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.cpp:16
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:22
cover_filter.h
Filters for the Coverage Instrumentation.
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196