CBMC
cover_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Coverage Instrumentation
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H
13 #define CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H
14 
16 
17 bool is_condition(const exprt &src);
18 
19 void collect_conditions_rec(const exprt &src, std::set<exprt> &dest);
20 
21 std::set<exprt> collect_conditions(const exprt &src);
22 
23 std::set<exprt> collect_conditions(const goto_programt::const_targett t);
24 
25 void collect_operands(const exprt &src, std::vector<exprt> &dest);
26 
27 void collect_decisions_rec(const exprt &src, std::set<exprt> &dest);
28 
29 std::set<exprt> collect_decisions(const exprt &src);
30 
31 std::set<exprt> collect_decisions(const goto_programt::const_targett t);
32 
33 #endif // CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H
Base class for all expressions.
Definition: expr.h:56
instructionst::const_iterator const_targett
Definition: goto_program.h:615
std::set< exprt > collect_decisions(const exprt &src)
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
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
Concrete Goto Program.