Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
80 void add(std::unique_ptr<function_filter_baset> filter)
82 filters.push_back(std::move(filter));
92 for(
const auto &filter :
filters)
93 if(!(*filter)(identifier, goto_function))
103 for(
const auto &filter :
filters)
104 filter->report_anomalies();
108 std::vector<std::unique_ptr<function_filter_baset>>
filters;
117 void add(std::unique_ptr<goal_filter_baset> filter)
119 filters.push_back(std::move(filter));
126 for(
const auto &filter :
filters)
127 if(!(*filter)(source_location))
137 for(
const auto &filter :
filters)
138 filter->report_anomalies();
142 std::vector<std::unique_ptr<goal_filter_baset>>
filters;
201 const std::string &cover_include_pattern)
241 #endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
Class that provides messages with a built-in verbosity 'level'.
virtual bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const =0
Returns true if the function passes the filter criteria.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool operator()(const source_locationt &source_location) const
Applies the filters to the given source location.
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.
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 symbolt &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.
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Call a goto_program non-trivial if it has:
single_function_filtert(message_handlert &message_handler, const irep_idt &function_id)
virtual ~function_filter_baset()
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.
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.
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
bool operator()(const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
Filter functions whose name matches the regex.
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.
function_filter_baset(message_handlert &message_handler)
file_filtert(message_handlert &message_handler, const irep_idt &file_id)
A collection of function filters to be applied in conjunction.
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.
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.