CBMC
|
Path coverage instrumenter. More...
#include <cover_instrument.h>
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_filterst & | goal_filters |
Path coverage instrumenter.
Definition at line 231 of file cover_instrument.h.
|
inline |
Definition at line 234 of file cover_instrument.h.
|
overrideprotectedvirtual |
Override this method to implement an instrumenter.
Implements cover_instrumenter_baset.
Definition at line 20 of file cover_instrument_other.cpp.