cprover
cover_instrument_other.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #include "cover_instrument.h"
13 
14 #include <util/cprover_prefix.h>
15 
16 #include <langapi/language_util.h>
17 
18 #include <algorithm>
19 
21  const irep_idt &,
22  goto_programt &,
24  const cover_blocks_baset &,
25  const assertion_factoryt &) const
26 {
27  if(is_non_cover_assertion(i_it))
28  i_it->turn_into_skip();
29 
30  // TODO: implement
31 }
32 
34  const irep_idt &function_id,
35  goto_programt &,
37  const cover_blocks_baset &,
38  const assertion_factoryt &) const
39 {
40  // turn into 'assert(false)' to avoid simplification
41  if(is_non_cover_assertion(i_it))
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,
51  goto_programt &,
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) + "'";
68  initialize_source_location(i_it, comment, function_id);
69  }
70  }
71  else if(is_non_cover_assertion(i_it))
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  });
86  INVARIANT(
87  last_function_call != goto_program.instructions.rend(),
88  "Goto program should have at least one function call");
89  INVARIANT(
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.set_comment(comment);
99  if_it->source_location.set_property_class("reachability_constraint");
100  if_it->source_location.set_function(function_id);
101 }
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
const source_locationt & source_location() const
Definition: expr.h:230
The Boolean constant false.
Definition: std_expr.h:2811
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
instructionst::iterator targett
Definition: goto_program.h:646
Boolean negation.
Definition: std_expr.h:2127
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:49
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)
Definition: race_check.cpp:109
#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