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 <langapi/language_util.h>
15 
16 #include "cover_util.h"
17 
19  const irep_idt &,
20  goto_programt &,
22  const cover_blocks_baset &,
23  const assertion_factoryt &) const
24 {
25  if(is_non_cover_assertion(i_it))
26  i_it->turn_into_skip();
27 
28  // TODO: implement
29 }
30 
32  const irep_idt &function_id,
33  goto_programt &,
35  const cover_blocks_baset &,
36  const assertion_factoryt &) const
37 {
38  // turn into 'assert(false)' to avoid simplification
39  if(is_non_cover_assertion(i_it))
40  {
41  i_it->guard = false_exprt();
43  i_it, id2string(i_it->source_location.get_comment()), function_id);
44  }
45 }
46 
48  const irep_idt &function_id,
49  goto_programt &,
51  const cover_blocks_baset &,
52  const assertion_factoryt &make_assertion) const
53 {
54  // turn __CPROVER_cover(x) into 'assert(!x)'
55  if(i_it->is_function_call())
56  {
57  const code_function_callt &code_function_call = i_it->get_function_call();
58  if(
59  code_function_call.function().id() == ID_symbol &&
60  to_symbol_expr(code_function_call.function()).get_identifier() ==
61  CPROVER_PREFIX "cover" &&
62  code_function_call.arguments().size() == 1)
63  {
64  const exprt c = code_function_call.arguments()[0];
65  *i_it = make_assertion(not_exprt(c), i_it->source_location);
66  std::string comment = "condition '" + from_expr(ns, function_id, c) + "'";
67  initialize_source_location(i_it, comment, function_id);
68  }
69  }
70  else if(is_non_cover_assertion(i_it))
71  i_it->turn_into_skip();
72 }
73 
75  const irep_idt &function_id,
76  goto_programt &goto_program,
78 {
79  const auto last_function_call = std::find_if(
80  goto_program.instructions.rbegin(),
81  goto_program.instructions.rend(),
82  [](const goto_programt::instructiont &instruction) {
83  return instruction.is_function_call();
84  });
85  INVARIANT(
86  last_function_call != goto_program.instructions.rend(),
87  "Goto program should have at least one function call");
88  INVARIANT(
89  last_function_call != goto_program.instructions.rbegin(),
90  "Goto program shouldn't end with a function call");
91  const auto if_it = last_function_call.base();
92  const auto location = if_it->source_location;
93  const std::string &comment =
94  "additional goal to ensure reachability of end of function";
95  goto_program.insert_before_swap(if_it);
96  *if_it = make_assertion(false_exprt(), location);
97  if_it->source_location.set_comment(comment);
98  if_it->source_location.set_property_class("reachability_constraint");
99  if_it->source_location.set_function(function_id);
100 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cover_instrumenter_baset::is_non_cover_assertion
bool is_non_cover_assertion(goto_programt::const_targett t) const
Definition: cover_instrument.h:93
cover_instrumenter_baset::initialize_source_location
void initialize_source_location(goto_programt::targett t, const std::string &comment, const irep_idt &function_id) const
Definition: cover_instrument.h:82
cover_instrument_end_of_function
void cover_instrument_end_of_function(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Definition: cover_instrument_other.cpp:74
cover_instrumenter_baset::ns
const namespacet ns
Definition: cover_instrument.h:71
exprt
Base class for all expressions.
Definition: expr.h:54
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
cover_cover_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:47
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
language_util.h
cover_assertion_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:31
cover_instrument.h
Coverage Instrumentation.
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
cover_blocks_baset
Definition: cover_basic_blocks.h:24
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
cover_instrumenter_baset::assertion_factoryt
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
Definition: cover_instrument.h:41
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
cover_path_instrumentert::instrument
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.
Definition: cover_instrument_other.cpp:18
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
cover_util.h
Coverage Instrumentation Utilities.
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
not_exprt
Boolean negation.
Definition: std_expr.h:2041