41 else if(
i_it->is_assert())
43 const auto location =
i_it->source_location();
45 if(location.get_property_class() !=
"coverage")
47 i_it->turn_into_skip();
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Coverage Instrumentation.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
API to expression classes.