Loading...

Searching...

No Matches

guard_expr.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_EXPR_H

13#define CPROVER_ANALYSES_GUARD_EXPR_H

14

15#include <util/std_expr.h>

16

19 struct guard_expr_managert

20{

21};

22

23 class guard_exprt

24{

25public:

29 explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e)

30 {

31 }

32

33 guard_exprt &operator=(const guard_exprt &other)

34 {

35 expr = other.expr;

36 return *this;

37 }

38

39 void add(const exprt &expr);

40

41 void append(const guard_exprt &guard)

42 {

43 add(guard.as_expr());

44 }

45

46 exprt as_expr() const

47{

48 return expr;

49 }

50

54 static constexpr bool is_always_simplified = false;

55

58 exprt guard_expr(exprt expr) const;

59

60 bool is_true() const

61{

62 return expr == true;

63 }

64

65 bool is_false() const

66{

67 return expr == false;

68 }

69

70 friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2);

71 friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2);

72

76 bool disjunction_may_simplify(const guard_exprt &other_guard);

77

78private:

79 exprt expr;

80};

81

82#endif // CPROVER_ANALYSES_GUARD_EXPR_H

guard

static exprt guard(const exprt::operandst &guards, exprt cond)

Definition c_safety_checks.cpp:69

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

exprt

Base class for all expressions.

Definition expr.h:57

guard_exprt

Definition guard_expr.h:24

guard_exprt::operator=

guard_exprt & operator=(const guard_exprt &other)

Definition guard_expr.h:33

guard_exprt::add

void add(const exprt &expr)

Definition guard_expr.cpp:38

guard_exprt::is_true

bool is_true() const

Definition guard_expr.h:60

guard_exprt::append

void append(const guard_exprt &guard)

Definition guard_expr.h:41

guard_exprt::disjunction_may_simplify

bool disjunction_may_simplify(const guard_exprt &other_guard)

Returns true if operator|= with other_guard may result in a simpler expression.

Definition guard_expr.cpp:123

guard_exprt::as_expr

exprt as_expr() const

Definition guard_expr.h:46

guard_exprt::guard_exprt

guard_exprt(const exprt &e, guard_expr_managert &)

Construct a BDD from an expression The guard_managert parameter is not used, but we keep it for unifo...

Definition guard_expr.h:29

guard_exprt::operator|=

friend guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)

Definition guard_expr.cpp:134

guard_exprt::is_false

bool is_false() const

Definition guard_expr.h:65

guard_exprt::operator-=

friend guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)

Definition guard_expr.cpp:64

guard_exprt::guard_expr

exprt guard_expr(exprt expr) const

Return guard => dest or a simplified variant thereof if either guard or dest are trivial.

Definition guard_expr.cpp:18

guard_exprt::expr

exprt expr

Definition guard_expr.h:79

guard_exprt::is_always_simplified

static constexpr bool is_always_simplified

The result of as_expr is not always in a simplified form and may requires some simplification.

Definition guard_expr.h:54

std_expr.h

API to expression classes.

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_expr.h Source File