CBMC
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 
18 
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 
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 
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 
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 
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 
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 }
bool empty() const
Definition: dstring.h:89
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.
irep_idt file_id
Definition: cover_filter.h:154
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name matches the regex.
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.
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
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.
const irep_idt & get_file() const
static bool is_built_in(const std::string &s)
Symbol table entry.
Definition: symbol.h:28
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Filters for the Coverage Instrumentation.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
#define INITIALIZE_FUNCTION
Symbol table entry.