12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H
47 "`assertion_factoryt` is expected to have the same type as "
48 "`goto_programt::make_assertion`.");
64 instrument(function_id, goto_program, i_it, basic_blocks, make_assertion);
96 return t->is_assert() &&
123 (*instrumenter)(function_id, goto_program, basic_blocks, make_assertion);
Assertion coverage instrumenter.
cover_assertion_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
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.
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.
cover_assume_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
Branch coverage instrumenter.
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.
cover_branch_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
Condition coverage instrumenter.
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.
cover_condition_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
__CPROVER_cover coverage instrumenter
cover_cover_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
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.
Decision coverage instrumenter.
cover_decision_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
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.
Base class for goto program coverage instrumenters.
const irep_idt property_class
virtual void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const =0
Override this method to implement an instrumenter.
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.
const goal_filterst & goal_filters
const irep_idt coverage_criterion
bool is_non_cover_assertion(goto_programt::const_targett t) const
virtual ~cover_instrumenter_baset()=default
void initialize_source_location(source_locationt &source_location, const std::string &comment, const irep_idt &function_id) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
A collection of instrumenters to be run.
std::vector< std::unique_ptr< cover_instrumenter_baset > > instrumenters
void operator()(const irep_idt &function_id, goto_programt &goto_program, const cover_blocks_baset &basic_blocks, const cover_instrumenter_baset::assertion_factoryt &make_assertion) const
Applies all instrumenters to the given goto program.
void add_from_criterion(coverage_criteriont, const symbol_table_baset &, const goal_filterst &)
Create and add an instrumenter based on the given criterion.
Basic block coverage instrumenter.
cover_location_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
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.
MC/DC coverage instrumenter.
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.
cover_mcdc_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
Path coverage instrumenter.
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.
cover_path_instrumentert(const symbol_table_baset &_symbol_table, const goal_filterst &_goal_filters)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goal filters to be applied in conjunction.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
void set(const irep_idt &name, const irep_idt &value)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
The symbol table base class interface.
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &)
#define Forall_goto_program_instructions(it, program)
static std::string comment(const rw_set_baset::entryt &entry, bool write)