cover_filter.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Coverage Instrumentation
 
Author: Daniel Kroening
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
#define CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H
 
#include <regex>
#include <memory>
 
#include <goto-programs/goto_functions.h>
 
class function_filter_baset
{
public:
  virtual ~function_filter_baset()
  {
  }
 
  virtual bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const = 0;
 
  virtual void report_anomalies() const
  {
    // do nothing by default
  }
};
 
class goal_filter_baset
{
public:
  virtual ~goal_filter_baset()
  {
  }
 
  virtual bool operator()(const source_locationt &) const = 0;
 
  virtual void report_anomalies() const
  {
    // do nothing by default
  }
};
 
class function_filterst
{
public:
  void add(std::unique_ptr<function_filter_baset> filter)
  {
    filters.push_back(std::move(filter));
  }
 
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const
  {
    for(const auto &filter : filters)
      if(!(*filter)(identifier, goto_function))
        return false;
 
    return true;
  }
 
  void report_anomalies() const
  {
    for(const auto &filter : filters)
      filter->report_anomalies();
  }
 
private:
  std::vector<std::unique_ptr<function_filter_baset>> filters;
};
 
class goal_filterst
{
public:
  void add(std::unique_ptr<goal_filter_baset> filter)
  {
    filters.push_back(std::move(filter));
  }
 
  bool operator()(const source_locationt &source_location) const
  {
    for(const auto &filter : filters)
      if(!(*filter)(source_location))
        return false;
 
    return true;
  }
 
  void report_anomalies() const
  {
    for(const auto &filter : filters)
      filter->report_anomalies();
  }
 
private:
  std::vector<std::unique_ptr<goal_filter_baset>> filters;
};
 
class internal_functions_filtert : public function_filter_baset
{
public:
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const override;
};
 
class file_filtert : public function_filter_baset
{
public:
  explicit file_filtert(const irep_idt &file_id) : file_id(file_id)
  {
  }
 
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const override;
 
private:
  irep_idt file_id;
};
 
class single_function_filtert : public function_filter_baset
{
public:
  explicit single_function_filtert(const irep_idt &function_id)
    : function_id(function_id)
  {
  }
 
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const override;
 
private:
  irep_idt function_id;
};
 
class include_pattern_filtert : public function_filter_baset
{
public:
  explicit include_pattern_filtert(const std::string &cover_include_pattern)
    : regex_matcher(cover_include_pattern)
  {
  }
 
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const override;
 
private:
  std::regex regex_matcher;
};
 
class trivial_functions_filtert : public function_filter_baset
{
public:
  bool operator()(
    const symbolt &identifier,
    const goto_functionst::goto_functiont &goto_function) const override;
};
 
class internal_goals_filtert : public goal_filter_baset
{
public:
  bool operator()(const source_locationt &) const override;
};
 
#endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H