CBMC
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_ANALYSES_GUARD_H
13
#define CPROVER_ANALYSES_GUARD_H
14
15
#ifdef BDD_GUARDS
16
17
#include "
guard_bdd.h
"
18
19
using
guard_managert
=
bdd_exprt
;
20
using
guardt
=
guard_bddt
;
21
22
#else
23
24
#include "
guard_expr.h
"
25
26
using
guard_managert
=
guard_expr_managert
;
27
using
guardt
=
guard_exprt
;
28
29
#endif // BDD_GUARDS
30
31
#endif // CPROVER_ANALYSES_GUARD_H
guard_exprt
Definition:
guard_expr.h:23
guard_bddt
Definition:
guard_bdd.h:21
bdd_exprt
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
Definition:
bdd_expr.h:33
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition:
guard_expr.h:19
guard_bdd.h
guard_expr.h
src
analyses
guard.h
Generated by
1.8.17