CBMC
Public Member Functions | List of all members
trivial_functions_filtert Class Reference

Filters out trivial functions. More...

#include <cover_filter.h>

+ Inheritance diagram for trivial_functions_filtert:
+ Collaboration diagram for trivial_functions_filtert:

Public Member Functions

bool operator() (const symbolt &identifier, const goto_functionst::goto_functiont &goto_function) const override
 Call a goto_program non-trivial if it has: More...
 
- Public Member Functions inherited from function_filter_baset
virtual ~function_filter_baset ()
 
virtual void report_anomalies () const
 Can be called after final filter application to report on unexpected situations encountered. More...
 

Detailed Description

Filters out trivial functions.

Definition at line 189 of file cover_filter.h.

Member Function Documentation

◆ operator()()

bool trivial_functions_filtert::operator() ( const symbolt &  function,
const goto_functionst::goto_functiont &  goto_function 
) const
overridevirtual

Call a goto_program non-trivial if it has:

  • Any declarations
  • At least 2 branches
  • At least 5 assignments These criteria are arbitrarily chosen.
    Parameters
    functionfunction symbol for function corresponding to goto_function
    goto_functiona goto function
    Returns
    returns true if non-trivial

Implements function_filter_baset.

Definition at line 100 of file cover_filter.cpp.

The documentation for this class was generated from the following files: