CBMC
cover_path_instrumentert Class Reference

Path coverage instrumenter. More...

#include <cover_instrument.h>

+ Inheritance diagram for cover_path_instrumentert:
+ Collaboration diagram for cover_path_instrumentert:

Public Member Functions

 cover_path_instrumentert (const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
 
- Public Member Functions inherited from cover_instrumenter_baset
virtual ~cover_instrumenter_baset ()=default
 
 cover_instrumenter_baset (const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
 
void operator() (const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const assertion_factoryt &make_assertion) const
 Instruments a goto program. More...
 

Protected Member Functions

void instrument (const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
 Override this method to implement an instrumenter. More...
 
- Protected Member Functions inherited from cover_instrumenter_baset
void initialize_source_location (source_locationt &source_location, const std::string &comment, const irep_idt &function_id) const
 
bool is_non_cover_assertion (goto_programt::const_targett t) const
 

Additional Inherited Members

- Public Types inherited from cover_instrumenter_baset
using assertion_factoryt = std::function< goto_programt::instructiont(const exprt &, const source_locationt &)>
 The type of function used to make goto_program assertions. More...
 
- Public Attributes inherited from cover_instrumenter_baset
const irep_idt property_class = "coverage"
 
const irep_idt coverage_criterion
 
- Protected Attributes inherited from cover_instrumenter_baset
const namespacet ns
 
const goal_filterstgoal_filters
 

Detailed Description

Path coverage instrumenter.

Definition at line 231 of file cover_instrument.h.

Constructor & Destructor Documentation

◆ cover_path_instrumentert()

cover_path_instrumentert::cover_path_instrumentert ( const symbol_table_baset _symbol_table,
const goal_filterst _goal_filters 
)
inline

Definition at line 234 of file cover_instrument.h.

Member Function Documentation

◆ instrument()

void cover_path_instrumentert::instrument ( const irep_idt function_id,
goto_programt ,
goto_programt::targett ,
const cover_blocks_baset ,
const assertion_factoryt  
) const
overrideprotectedvirtual

Override this method to implement an instrumenter.

Implements cover_instrumenter_baset.

Definition at line 20 of file cover_instrument_other.cpp.


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