Go to the documentation of this file.
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
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 irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name match the regex.
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.
std::vector< std::unique_ptr< goal_filter_baset > > filters
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const
Applies the filters to the given function.
void add(std::unique_ptr< goal_filter_baset > filter)
Adds a function filter.
virtual ~function_filter_baset()
bool operator()(const irep_idt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
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 void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.
Filters out goals with source locations considered internal.
internal_functions_filtert(message_handlert &message_handler)
virtual bool operator()(const source_locationt &) const =0
Returns true if the goal passes the filter criteria.
Base class for filtering functions.
Base class for filtering goals.
A collection of goal filters to be applied in conjunction.
include_pattern_filtert(message_handlert &message_handler, const std::string &cover_include_pattern)
internal_goals_filtert(message_handlert &message_handler)
Filters out CPROVER internal functions.
Filters functions that match the provided pattern.
::goto_functiont goto_functiont
trivial_functions_filtert(message_handlert &message_handler)
Filters out trivial functions.
goal_filter_baset(message_handlert &message_handler)
message_handlert * message_handler
std::vector< std::unique_ptr< function_filter_baset > > filters
virtual ~goal_filter_baset()
bool operator()(const source_locationt &) const override
Filter goals at source locations considered internal.
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.
function_filter_baset(message_handlert &message_handler)
A collection of function filters to be applied in conjunction.
void add(std::unique_ptr< function_filter_baset > filter)
Adds a function filter.
virtual void report_anomalies() const
Can be called after final filter application to report on unexpected situations encountered.