CBMC
cover_util.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_util.h"
13 
14 bool is_condition(const exprt &src)
15 {
16  if(!src.is_boolean())
17  return false;
18 
19  // conditions are 'atomic predicates'
20  if(
21  src.id() == ID_and || src.id() == ID_or || src.id() == ID_not ||
22  src.id() == ID_implies)
23  return false;
24 
25  return true;
26 }
27 
28 void collect_conditions_rec(const exprt &src, std::set<exprt> &dest)
29 {
30  if(src.id() == ID_address_of)
31  {
32  return;
33  }
34 
35  for(const auto &op : src.operands())
36  collect_conditions_rec(op, dest);
37 
38  if(is_condition(src) && !src.is_constant())
39  dest.insert(src);
40 }
41 
42 std::set<exprt> collect_conditions(const exprt &src)
43 {
44  std::set<exprt> result;
45  collect_conditions_rec(src, result);
46  return result;
47 }
48 
50 {
51  std::set<exprt> result;
52 
53  t->apply([&result](const exprt &e) { collect_conditions_rec(e, result); });
54 
55  return result;
56 }
57 
58 void collect_operands(const exprt &src, std::vector<exprt> &dest)
59 {
60  for(const exprt &op : src.operands())
61  {
62  if(op.id() == src.id())
63  collect_operands(op, dest);
64  else
65  dest.push_back(op);
66  }
67 }
68 
69 void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
70 {
71  if(src.id() == ID_address_of)
72  {
73  return;
74  }
75 
76  if(src.is_boolean())
77  {
78  if(src.is_constant())
79  {
80  // ignore me
81  }
82  else if(src.id() == ID_not)
83  {
84  collect_decisions_rec(to_not_expr(src).op(), dest);
85  }
86  else
87  {
88  dest.insert(src);
89  }
90  }
91  else
92  {
93  for(const auto &op : src.operands())
94  collect_decisions_rec(op, dest);
95  }
96 }
97 
99 {
100  std::set<exprt> result;
101 
102  t->apply([&result](const exprt &e) { collect_decisions_rec(e, result); });
103 
104  return result;
105 }
Base class for all expressions.
Definition: expr.h:56
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
instructionst::const_iterator const_targett
Definition: goto_program.h:615
const irep_idt & id() const
Definition: irep.h:384
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover_util.cpp:42
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover_util.cpp:69
std::set< exprt > collect_decisions(const goto_programt::const_targett t)
Definition: cover_util.cpp:98
void collect_conditions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover_util.cpp:28
void collect_operands(const exprt &src, std::vector< exprt > &dest)
Definition: cover_util.cpp:58
bool is_condition(const exprt &src)
Definition: cover_util.cpp:14
Coverage Instrumentation Utilities.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352