cprover
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.type().id() != ID_bool)
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  switch(t->type)
52  {
53  case GOTO:
54  case ASSERT:
55  return collect_conditions(t->guard);
56 
57  case ASSIGN:
58  case FUNCTION_CALL:
59  return collect_conditions(t->code);
60 
61  default:
62  {
63  }
64  }
65 
66  return std::set<exprt>();
67 }
68 
69 void collect_operands(const exprt &src, std::vector<exprt> &dest)
70 {
71  for(const exprt &op : src.operands())
72  {
73  if(op.id() == src.id())
74  collect_operands(op, dest);
75  else
76  dest.push_back(op);
77  }
78 }
79 
80 void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
81 {
82  if(src.id() == ID_address_of)
83  {
84  return;
85  }
86 
87  if(src.type().id() == ID_bool)
88  {
89  if(src.is_constant())
90  {
91  // ignore me
92  }
93  else if(src.id() == ID_not)
94  {
95  collect_decisions_rec(src.op0(), dest);
96  }
97  else
98  {
99  dest.insert(src);
100  }
101  }
102  else
103  {
104  for(const auto &op : src.operands())
105  collect_decisions_rec(op, dest);
106  }
107 }
108 
109 std::set<exprt> collect_decisions(const exprt &src)
110 {
111  std::set<exprt> result;
112  collect_decisions_rec(src, result);
113  return result;
114 }
115 
117 {
118  switch(t->type)
119  {
120  case GOTO:
121  case ASSERT:
122  return collect_decisions(t->guard);
123 
124  case ASSIGN:
125  case FUNCTION_CALL:
126  return collect_decisions(t->code);
127 
128  default:
129  {
130  }
131  }
132 
133  return std::set<exprt>();
134 }
std::set< exprt > collect_decisions(const exprt &src)
Definition: cover_util.cpp:109
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:69
exprt & op0()
Definition: expr.h:72
typet & type()
Definition: expr.h:56
bool is_condition(const exprt &src)
Definition: cover_util.cpp:14
const irep_idt & id() const
Definition: irep.h:189
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover_util.cpp:42
instructionst::const_iterator const_targett
Definition: goto_program.h:398
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover_util.cpp:80
Coverage Instrumentation Utilities.
bool is_constant() const
Definition: expr.cpp:119
Base class for all expressions.
Definition: expr.h:42
operandst & operands()
Definition: expr.h:66