CBMC
Loading...
Searching...
No Matches
cover_util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Coverage Instrumentation
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H
13#define CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H
14
16
17bool is_condition(const exprt &src);
18
19void collect_conditions_rec(const exprt &src, std::set<exprt> &dest);
20
21std::set<exprt> collect_conditions(const exprt &src);
22
24
25void collect_operands(const exprt &src, std::vector<exprt> &dest);
26
27void collect_decisions_rec(const exprt &src, std::set<exprt> &dest);
28
29std::set<exprt> collect_decisions(const exprt &src);
30
31std::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
void collect_decisions_rec(const exprt &src, std::set< exprt > &dest)
std::set< exprt > collect_decisions(const exprt &src)
void collect_conditions_rec(const exprt &src, std::set< exprt > &dest)
void collect_operands(const exprt &src, std::vector< exprt > &dest)
bool is_condition(const exprt &src)
std::set< exprt > collect_conditions(const exprt &src)
Concrete Goto Program.