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 
15 
21  const irep_idt &identifier,
22  const goto_functionst::goto_functiont &goto_function) const
23 {
24  if(identifier == goto_functionst::entry_point())
25  return false;
26 
27  if(identifier == INITIALIZE_FUNCTION)
28  return false;
29 
30  if(goto_function.is_hidden())
31  return false;
32 
33  // ignore Java built-ins (synthetic functions)
34  if(has_prefix(id2string(identifier), "java::array["))
35  return false;
36 
37  // ignore if built-in library
38  if(
39  !goto_function.body.instructions.empty() &&
40  goto_function.body.instructions.front().source_location.is_built_in())
41  return false;
42 
43  return true;
44 }
45 
51  const irep_idt &identifier,
52  const goto_functionst::goto_functiont &goto_function) const
53 {
54  (void)goto_function; // unused parameter
55  std::smatch string_matcher;
56  return std::regex_match(id2string(identifier), string_matcher, regex_matcher);
57 }
58 
68  const irep_idt &identifier,
69  const goto_functionst::goto_functiont &goto_function) const
70 {
71  (void)identifier; // unused parameter
72  unsigned long count_assignments = 0, count_goto = 0;
73  forall_goto_program_instructions(i_it, goto_function.body)
74  {
75  if(i_it->is_goto())
76  {
77  if((++count_goto) >= 2)
78  return true;
79  }
80  else if(i_it->is_assign())
81  {
82  if((++count_assignments) >= 5)
83  return true;
84  }
85  else if(i_it->is_decl())
86  return true;
87  }
88 
89  return false;
90 }
91 
96 operator()(const source_locationt &source_location) const
97 {
98  if(source_location.get_file().empty())
99  return false;
100 
101  if(source_location.is_built_in())
102  return false;
103 
104  return true;
105 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
static bool is_built_in(const std::string &s)
#define INITIALIZE_FUNCTION
::goto_functiont goto_functiont
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name match the regex.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
const irep_idt & get_file() const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
Filters for the Coverage Instrumentation.
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter out functions that are not considered provided by the user.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
bool empty() const
Definition: dstring.h:75