cprover
cover_instrumenter_baset Class Referenceabstract

Base class for goto program coverage instrumenters. More...

#include <cover_instrument.h>

Inheritance diagram for cover_instrumenter_baset:
[legend]
Collaboration diagram for cover_instrumenter_baset:
[legend]

Public Member Functions

virtual ~cover_instrumenter_baset ()=default
 
 cover_instrumenter_baset (const symbol_tablet &_symbol_table, const goal_filterst &_goal_filters, const irep_idt &_coverage_criterion)
 
virtual void operator() (goto_programt &goto_program, const cover_blocks_baset &basic_blocks) const
 Instruments a goto program. More...
 

Public Attributes

const irep_idt property_class = "coverage"
 
const irep_idt coverage_criterion
 

Protected Member Functions

virtual void instrument (goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const =0
 Override this method to implement an instrumenter. More...
 
void initialize_source_location (goto_programt::targett t, const std::string &comment, const irep_idt &function) const
 
bool is_non_cover_assertion (goto_programt::const_targett t) const
 

Protected Attributes

const namespacet ns
 
const goal_filterstgoal_filters
 

Detailed Description

Base class for goto program coverage instrumenters.

Definition at line 25 of file cover_instrument.h.

Constructor & Destructor Documentation

◆ ~cover_instrumenter_baset()

virtual cover_instrumenter_baset::~cover_instrumenter_baset ( )
virtualdefault

◆ cover_instrumenter_baset()

cover_instrumenter_baset::cover_instrumenter_baset ( const symbol_tablet _symbol_table,
const goal_filterst _goal_filters,
const irep_idt _coverage_criterion 
)
inline

Definition at line 29 of file cover_instrument.h.

Member Function Documentation

◆ initialize_source_location()

◆ instrument()

virtual void cover_instrumenter_baset::instrument ( goto_programt ,
goto_programt::targett ,
const cover_blocks_baset  
) const
protectedpure virtual

◆ is_non_cover_assertion()

◆ operator()()

virtual void cover_instrumenter_baset::operator() ( goto_programt goto_program,
const cover_blocks_baset basic_blocks 
) const
inlinevirtual

Instruments a goto program.

Parameters
goto_programa goto program
basic_blocksdetected basic blocks

Definition at line 42 of file cover_instrument.h.

References Forall_goto_program_instructions, goto_program, and instrument().

Member Data Documentation

◆ coverage_criterion

const irep_idt cover_instrumenter_baset::coverage_criterion

◆ goal_filters

const goal_filterst& cover_instrumenter_baset::goal_filters
protected

Definition at line 57 of file cover_instrument.h.

Referenced by cover_location_instrumentert::instrument().

◆ ns

◆ property_class

const irep_idt cover_instrumenter_baset::property_class = "coverage"

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