12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H 13 #define CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H 79 void add(std::unique_ptr<function_filter_baset> filter)
81 filters.push_back(std::move(filter));
91 for(
const auto &filter :
filters)
92 if(!(*filter)(identifier, goto_function))
102 for(
const auto &filter :
filters)
103 filter->report_anomalies();
107 std::vector<std::unique_ptr<function_filter_baset>>
filters;
116 void add(std::unique_ptr<goal_filter_baset> filter)
118 filters.push_back(std::move(filter));
125 for(
const auto &filter :
filters)
126 if(!(*filter)(source_location))
136 for(
const auto &filter :
filters)
137 filter->report_anomalies();
141 std::vector<std::unique_ptr<goal_filter_baset>>
filters;
164 const std::string &cover_include_pattern)
204 #endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H function_filter_baset(message_handlert &message_handler)
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
A collection of function filters to be applied in conjunction.
Filters out CPROVER internal functions.
include_pattern_filtert(message_handlert &message_handler, const std::string &cover_include_pattern)
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const
Applies the filters to the given function.
Filters functions that match the provided pattern.
trivial_functions_filtert(message_handlert &message_handler)
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
virtual ~function_filter_baset()
virtual ~goal_filter_baset()
Filters out goals with source locations considered internal.
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
::goto_functiont goto_functiont
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name match the regex.
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
Base class for filtering functions.
goal_filter_baset(message_handlert &message_handler)
Base class for filtering goals.
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 out trivial functions.
internal_goals_filtert(message_handlert &message_handler)
std::vector< std::unique_ptr< function_filter_baset > > filters
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
internal_functions_filtert(message_handlert &message_handler)
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.
virtual bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const =0
Returns true if the function passes the filter criteria.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
message_handlert * message_handler
A collection of goal filters to be applied in conjunction.
std::vector< std::unique_ptr< goal_filter_baset > > filters
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.