guard_exprt Class Reference

#include <guard_expr.h>

Collaboration diagram for guard_exprt:

Public Member Functions
	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 uniformity with other implementations of guards which may use it.
guard_exprt &	operator= (const guard_exprt &other)
void	add (const exprt &expr)
void	append (const guard_exprt &guard)
exprt	as_expr () const
exprt	guard_expr (exprt expr) const
	Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
bool	is_true () const
bool	is_false () const
bool	disjunction_may_simplify (const guard_exprt &other_guard)
	Returns true if operator|= with other_guard may result in a simpler expression.

Static Public Attributes
static constexpr bool	is_always_simplified = false
	The result of as_expr is not always in a simplified form and may requires some simplification.

Private Attributes
exprt	expr

Friends
guard_exprt &	operator-= (guard_exprt &g1, const guard_exprt &g2)
guard_exprt &	operator|= (guard_exprt &g1, const guard_exprt &g2)

Detailed Description

Definition at line 23 of file guard_expr.h.

Constructor & Destructor Documentation

guard_exprt()

guard_exprt::guard_exprt ( const exprt &  e, guard_expr_managert &    )

inlineexplicit

Construct a BDD from an expression The guard_managert parameter is not used, but we keep it for uniformity with other implementations of guards which may use it.

Definition at line 29 of file guard_expr.h.

Member Function Documentation

add()

void guard_exprt::add

(

const exprt &

expr

)

Definition at line 38 of file guard_expr.cpp.

append()

void guard_exprt::append ( const guard_exprt &  guard )

inline

Definition at line 41 of file guard_expr.h.

as_expr()

exprt guard_exprt::as_expr ( ) const

inline

Definition at line 46 of file guard_expr.h.

disjunction_may_simplify()

bool guard_exprt::disjunction_may_simplify

(

const guard_exprt &

other_guard

)

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

For guard_exprt in practice this means they're both conjunctions, since for other things we just OR them together.

Definition at line 123 of file guard_expr.cpp.

guard_expr()

exprt guard_exprt::guard_expr

(

exprt

expr

)

const

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

Definition at line 18 of file guard_expr.cpp.

is_false()

bool guard_exprt::is_false ( ) const

inline

Definition at line 65 of file guard_expr.h.

is_true()

bool guard_exprt::is_true ( ) const

inline

Definition at line 60 of file guard_expr.h.

operator=()

guard_exprt & guard_exprt::operator= ( const guard_exprt &  other )

inline

Definition at line 33 of file guard_expr.h.

Friends And Related Symbol Documentation

operator-=

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

friend

Definition at line 64 of file guard_expr.cpp.

operator|=

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

friend

Definition at line 134 of file guard_expr.cpp.

Member Data Documentation

expr

exprt guard_exprt::expr

private

Definition at line 79 of file guard_expr.h.

is_always_simplified

constexpr bool guard_exprt::is_always_simplified = false

staticconstexpr

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

This can vary according to the guard implementation.

Definition at line 54 of file guard_expr.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/analyses/guard_expr.h
• /home/runner/work/cbmc/cbmc/src/analyses/guard_expr.cpp