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 
20 using guardt = guard_bddt;
21 
22 #else
23 
24 #include "guard_expr.h"
25 
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