cprover
Loading...
Searching...
No Matches
cover_condition_instrumentert Class Reference

Condition coverage instrumenter. More...

#include <cover_instrument.h>

Inheritance diagram for cover_condition_instrumentert:
Collaboration diagram for cover_condition_instrumentert:

Public Member Functions

 cover_condition_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.

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.
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
 The type of function used to make goto_program assertions.
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

Condition coverage instrumenter.

Definition at line 171 of file cover_instrument.h.

Constructor & Destructor Documentation

◆ cover_condition_instrumentert()

cover_condition_instrumentert::cover_condition_instrumentert ( const symbol_table_baset & _symbol_table,
const goal_filterst & _goal_filters )
inline

Definition at line 174 of file cover_instrument.h.

Member Function Documentation

◆ instrument()

void cover_condition_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 18 of file cover_instrument_condition.cpp.


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