cprover
Loading...
Searching...
No Matches
cover_instrument_other.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "cover_instrument.h"
13
14#include <util/cprover_prefix.h>
15
17
18#include <algorithm>
19
21 const irep_idt &,
24 const cover_blocks_baset &,
25 const assertion_factoryt &) const
26{
28 i_it->turn_into_skip();
29
30 // TODO: implement
31}
32
34 const irep_idt &function_id,
37 const cover_blocks_baset &,
38 const assertion_factoryt &) const
39{
40 // turn into 'assert(false)' to avoid simplification
42 {
43 i_it->guard = false_exprt();
45 i_it, id2string(i_it->source_location().get_comment()), function_id);
46 }
47}
48
50 const irep_idt &function_id,
53 const cover_blocks_baset &,
54 const assertion_factoryt &make_assertion) const
55{
56 // turn __CPROVER_cover(x) into 'assert(!x)'
57 if(i_it->is_function_call())
58 {
59 const auto &function = i_it->call_function();
60 if(
61 function.id() == ID_symbol &&
62 to_symbol_expr(function).get_identifier() == CPROVER_PREFIX "cover" &&
63 i_it->call_arguments().size() == 1)
64 {
65 const exprt c = i_it->call_arguments()[0];
66 *i_it = make_assertion(not_exprt(c), i_it->source_location());
67 std::string comment = "condition '" + from_expr(ns, function_id, c) + "'";
69 }
70 }
72 i_it->turn_into_skip();
73}
74
76 const irep_idt &function_id,
77 goto_programt &goto_program,
79{
80 const auto last_function_call = std::find_if(
81 goto_program.instructions.rbegin(),
82 goto_program.instructions.rend(),
83 [](const goto_programt::instructiont &instruction) {
84 return instruction.is_function_call();
85 });
87 last_function_call != goto_program.instructions.rend(),
88 "Goto program should have at least one function call");
90 last_function_call != goto_program.instructions.rbegin(),
91 "Goto program shouldn't end with a function call");
92 const auto if_it = last_function_call.base();
93 const auto location = if_it->source_location();
94 const std::string &comment =
95 "additional goal to ensure reachability of end of function";
96 goto_program.insert_before_swap(if_it);
97 *if_it = make_assertion(false_exprt(), location);
98 if_it->source_location_nonconst().set_comment(comment);
99 if_it->source_location_nonconst().set_property_class(
100 "reachability_constraint");
101 if_it->source_location_nonconst().set_function(function_id);
102}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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 &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
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
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
The Boolean constant false.
Definition std_expr.h:2865
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
Boolean negation.
Definition std_expr.h:2181
Coverage Instrumentation.
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189