27 if(!i_it->source_location.is_built_in())
33 for(
const auto &d : decisions)
35 const std::string d_string =
from_expr(
ns, i_it->function, d);
37 const std::string comment_t =
"decision `" + d_string +
"' true";
38 const irep_idt function = i_it->function;
40 i_it->make_assertion(d);
41 i_it->source_location = source_location;
44 const std::string comment_f =
"decision `" + d_string +
"' false";
47 i_it->source_location = source_location;
52 for(std::size_t i = 0; i < decisions.size() * 2; i++)
std::set< exprt > collect_decisions(const exprt &src)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Coverage Instrumentation.
instructionst::iterator targett
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
Coverage Instrumentation Utilities.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A generic container class for the GOTO intermediate representation of one function.
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function) const
bool is_non_cover_assertion(goto_programt::const_targett t) const