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

#include <cover_instrument.h>

Inheritance diagram for cover_assume_instrumentert:
Collaboration diagram for cover_assume_instrumentert:

Public Member Functions

 cover_assume_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 &, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
 Instrument program to check coverage of assume statements.
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

Definition at line 296 of file cover_instrument.h.

Constructor & Destructor Documentation

◆ cover_assume_instrumentert()

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

Definition at line 299 of file cover_instrument.h.

Member Function Documentation

◆ instrument()

void cover_assume_instrumentert::instrument ( const irep_idt & function_id,
goto_programt & goto_program,
goto_programt::targett & i_it,
const cover_blocks_baset & ,
const assertion_factoryt & make_assertion ) const
overrideprotectedvirtual

Instrument program to check coverage of assume statements.

Parameters
function_idThe name of the function under instrumentation.
goto_programThe goto-program (function under instrumentation).
i_itThe current instruction (instruction under instrumentation).
make_assertionThe assertion generator function.

Implements cover_instrumenter_baset.

Definition at line 16 of file cover_instrument_assume.cpp.


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