Loading...

Searching...

No Matches

guard.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module: Guard Data Structure

4

5Author: 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 <solvers/prop/bdd_expr.h>

18

19# include "guard_bdd.h"

20

21using guard_managert = bdd_exprt;

22using guardt = guard_bddt;

23

24#else

25

26#include "guard_expr.h"

27

28 using guard_managert = guard_expr_managert;

29 using guardt = guard_exprt;

30

31#endif // BDD_GUARDS

32

33#endif // CPROVER_ANALYSES_GUARD_H

bdd_expr.h

Conversion between exprt and miniBDD.

bdd_exprt

Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...

Definition bdd_expr.h:34

guard_bddt

Definition guard_bdd.h:22

guard_exprt

Definition guard_expr.h:24

guard_bdd.h

Guard Data Structure Implementation using BDDs.

guard_expr.h

Guard Data Structure.

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:20

CBMC: /home/runner/work/cbmc/cbmc/src/analyses/guard.h Source File