cprover
guard.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Guard Data Structure
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_UTIL_GUARD_H
13
#define CPROVER_UTIL_GUARD_H
14
15
#include <iosfwd>
16
17
#include "
std_expr.h
"
18
19
class
guardt
:
public
exprt
20
{
21
public
:
22
guardt
()
23
{
24
*
this
=
true_exprt
();
25
}
26
27
guardt
&
operator=
(
const
exprt
&e)
28
{
29
*
this
=static_cast<const guardt&>(e);
30
31
return
*
this
;
32
}
33
34
void
add
(
const
exprt
&expr);
35
36
void
append
(
const
guardt
&guard)
37
{
38
add
(guard);
39
}
40
41
exprt
as_expr
()
const
42
{
43
return
*
this
;
44
}
45
46
void
guard_expr
(
exprt
&dest)
const
;
47
48
friend
guardt
&
operator -=
(
guardt
&g1,
const
guardt
&g2);
49
friend
guardt
&
operator |=
(
guardt
&g1,
const
guardt
&g2);
50
};
51
52
#endif // CPROVER_UTIL_GUARD_H
guardt::add
void add(const exprt &expr)
Definition:
guard.cpp:43
guardt::operator-=
friend guardt & operator-=(guardt &g1, const guardt &g2)
Definition:
guard.cpp:72
exprt
Base class for all expressions.
Definition:
expr.h:54
guardt
Definition:
guard.h:19
guardt::operator|=
friend guardt & operator|=(guardt &g1, const guardt &g2)
Definition:
guard.cpp:101
guardt::guard_expr
void guard_expr(exprt &dest) const
Definition:
guard.cpp:21
guardt::append
void append(const guardt &guard)
Definition:
guard.h:36
guardt::operator=
guardt & operator=(const exprt &e)
Definition:
guard.h:27
guardt::as_expr
exprt as_expr() const
Definition:
guard.h:41
guardt::guardt
guardt()
Definition:
guard.h:22
true_exprt
The Boolean constant true.
Definition:
std_expr.h:4443
std_expr.h
util
guard.h
Generated by
1.8.16