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  goto_programt &,
21  const cover_blocks_baset &) const
22 {
23  if(is_non_cover_assertion(i_it))
24  i_it->make_skip();
25 
26  // TODO: implement
27 }
28 
30  goto_programt &,
32  const cover_blocks_baset &) const
33 {
34  // turn into 'assert(false)' to avoid simplification
35  if(is_non_cover_assertion(i_it))
36  {
37  i_it->guard = false_exprt();
39  i_it, id2string(i_it->source_location.get_comment()), i_it->function);
40  }
41 }
42 
44  goto_programt &,
46  const cover_blocks_baset &) const
47 {
48  // turn __CPROVER_cover(x) into 'assert(!x)'
49  if(i_it->is_function_call())
50  {
51  const code_function_callt &code_function_call =
52  to_code_function_call(i_it->code);
53  if(
54  code_function_call.function().id() == ID_symbol &&
55  to_symbol_expr(code_function_call.function()).get_identifier() ==
56  CPROVER_PREFIX "cover" &&
57  code_function_call.arguments().size() == 1)
58  {
59  const exprt c = code_function_call.arguments()[0];
60  std::string comment =
61  "condition `" + from_expr(ns, i_it->function, c) + "'";
62  i_it->guard = not_exprt(c);
63  i_it->type = ASSERT;
64  i_it->code.clear();
65  initialize_source_location(i_it, comment, i_it->function);
66  }
67  }
68  else if(is_non_cover_assertion(i_it))
69  i_it->make_skip();
70 }
71 
73  const irep_idt &function,
74  goto_programt &goto_program)
75 {
76  auto if_it = goto_program.instructions.end();
77  while(!if_it->is_function_call())
78  if_it--;
79  if_it++;
80  const std::string &comment =
81  "additional goal to ensure reachability of end of function";
82  goto_program.insert_before_swap(if_it);
83  if_it->make_assertion(false_exprt());
84  if_it->source_location.set_comment(comment);
85  if_it->source_location.set_property_class("reachability_constraint");
86  if_it->source_location.set_function(function);
87  if_it->function = function;
88 }
Boolean negation.
Definition: std_expr.h:3308
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
#define CPROVER_PREFIX
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void cover_instrument_end_of_function(const irep_idt &function, goto_programt &goto_program)
Coverage Instrumentation.
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:1109
instructionst::iterator targett
Definition: goto_program.h:414
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
codet representation of a function call statement.
Definition: std_code.h:1036
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Coverage Instrumentation Utilities.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
The Boolean constant false.
Definition: std_expr.h:4452
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
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
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173