Go to the documentation of this file.
24 i_it->turn_into_skip();
26 const bool is_function_entry_point =
28 const bool is_conditional_goto = i_it->is_goto() && !i_it->guard.is_true();
29 if(!is_function_entry_point && !is_conditional_goto)
35 if(is_function_entry_point)
39 std::string
comment =
"entry point";
44 i_it, make_assertion(
false_exprt(), source_location));
48 if(is_conditional_goto)
52 std::string true_comment =
"block " + b +
" branch true";
53 std::string false_comment =
"block " + b +
" branch false";
55 exprt guard = i_it->guard;
59 *i_it = make_assertion(
not_exprt(guard), source_location);
63 *i_it = make_assertion(guard, source_location);
66 std::advance(i_it, 2);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool is_non_cover_assertion(goto_programt::const_targett t) const
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
Base class for all expressions.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const goal_filterst & goal_filters
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Coverage Instrumentation.
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.
The Boolean constant false.
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
instructionst instructions
The list of instructions in the goto program.
Basic blocks detection for Coverage Instrumentation.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static std::string comment(const rw_set_baset::entryt &entry, bool write)
virtual std::size_t block_of(goto_programt::const_targett t) const =0
Filters for the Coverage Instrumentation.
instructionst::iterator targett