#include <cover_instrument.h>
|
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. More...
|
|
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. More...
|
|
void | initialize_source_location (goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const |
|
bool | is_non_cover_assertion (goto_programt::const_targett t) const |
|
Definition at line 297 of file cover_instrument.h.
◆ cover_assume_instrumentert()
cover_assume_instrumentert::cover_assume_instrumentert |
( |
const symbol_tablet & |
_symbol_table, |
|
|
const goal_filterst & |
_goal_filters |
|
) |
| |
|
inline |
◆ instrument()
Instrument program to check coverage of assume statements.
- Parameters
-
function_id | The name of the function under instrumentation. |
goto_program | The goto-program (function under instrumentation). |
i_it | The current instruction (instruction under instrumentation). |
make_assertion | The assertion generator function. |
Implements cover_instrumenter_baset.
Definition at line 17 of file cover_instrument_assume.cpp.
The documentation for this class was generated from the following files: