cprover
Loading...
Searching...
No Matches
cover_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "cover_util.h"
13
14bool 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
28void 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
42std::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
58void 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
69void 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.type().id() == ID_bool)
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:54
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
instructionst::const_iterator const_targett
Definition: goto_program.h:593
const irep_idt & id() const
Definition: irep.h:396
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
Definition: cover_util.cpp:69
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
std::set< exprt > collect_decisions(const goto_programt::const_targett t)
Definition: cover_util.cpp:98
bool is_condition(const exprt &src)
Definition: cover_util.cpp:14
std::set< exprt > collect_conditions(const exprt &src)
Definition: cover_util.cpp:42
Coverage Instrumentation Utilities.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206