guard2tc Class Reference

Path-condition guard container. More...

#include <irep2_guard.h>

Inheritance diagram for guard2tc:

Public Member Functions
	guard2tc ()=default
	guard2tc (const guard2tc &)=default
	guard2tc (guard2tc &&) noexcept=default
guard2tc &	operator= (const guard2tc &)=default
guard2tc &	operator= (guard2tc &&) noexcept=default
void	add (const expr2tc &expr)
void	append (const guard2tc &other)
expr2tc	as_expr () const
void	guard_expr (expr2tc &dest) const
bool	disjunction_may_simplify (const guard2tc &other) const
bool	is_true () const
bool	is_false () const
void	make_true ()
void	make_false ()
void	swap (guard2tc &)=delete
	Deleted.
void	dump () const
Public Member Functions inherited from irep_container< expr2t >
constexpr	irep_container () noexcept
	irep_container (const irep_container &ref) noexcept
	irep_container (irep_container &&ref) noexcept
	~irep_container ()
irep_container &	operator= (const irep_container &ref) noexcept
irep_container &	operator= (irep_container &&ref) noexcept
const expr2t &	operator* () const noexcept
const expr2t *	operator-> () const noexcept
const expr2t *	get () const noexcept
expr2t *	get ()
expr2t &	operator* ()
expr2t *	operator-> ()
	operator bool () const noexcept
void	reset () noexcept
void	detach ()
void	swap (irep_container &b) noexcept
irep_container	simplify () const
size_t	crc () const

Public Attributes
guard_seq	guard_list

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

Detailed Description

Path-condition guard container.

guard2tc extends expr2tc with a flat list of conjuncts (guard_list) accumulated along an execution path. Wherever an expr2tc is expected, a guard2tc works directly because it is an expr2tc.

Mutators maintain the expr2tc base incrementally as the and-chain of the current conjuncts (matching the historic guardt::g_expr/build_guard_expr split), so as_expr() and implicit conversions are pure reads. goto_symext::prefix_index keys a cache on this chain's nodes and relies on it being left-leaning. A default-constructed guard has an empty list and a nil base; as_expr() then short-circuits to gen_true_expr() without touching the base.

Invariant: guard_list is treated as a set of conjuncts — no duplicates are expected since x && x ≡ x. operator-= and operator|= use hash-set membership probes which give set rather than multiset semantics; symex's natural pattern of adding fresh branch symbols preserves uniqueness. Injecting the same conjunct twice leaves a logically-redundant duplicate in the list and weakens the set-op equality guarantees but does not produce unsound path conditions.

Constructor & Destructor Documentation

guard2tc() [1/3]

guard2tc::guard2tc ( )

default

guard2tc() [2/3]

guard2tc::guard2tc ( const guard2tc & )

default

guard2tc() [3/3]

guard2tc::guard2tc ( guard2tc && )

defaultnoexcept

Member Function Documentation

add()

void guard2tc::add

(

const expr2tc &

expr

)

append()

void guard2tc::append

(

const guard2tc &

other

)

as_expr()

expr2tc guard2tc::as_expr

(

)

const

disjunction_may_simplify()

bool guard2tc::disjunction_may_simplify

(

const guard2tc &

other

)

const

dump()

void guard2tc::dump

(

)

const

guard_expr()

void guard2tc::guard_expr

(

expr2tc &

dest

)

const

is_false()

bool guard2tc::is_false

(

)

const

is_true()

bool guard2tc::is_true

(

)

const

make_false()

void guard2tc::make_false

(

)

make_true()

void guard2tc::make_true

(

)

operator=() [1/2]

guard2tc & guard2tc::operator= ( const guard2tc & )

default

operator=() [2/2]

guard2tc & guard2tc::operator= ( guard2tc && )

defaultnoexcept

swap()

void guard2tc::swap ( guard2tc & )

delete

Deleted.

The inherited irep_container::swap would silently swap only the expr2tc base and leave guard_list desynced — use g = std::move(other) instead, which moves both members atomically and is one-way (cheaper than swap when the source goes out of scope immediately after).

Friends And Related Symbol Documentation

operator-=

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

friend

operator==

bool operator== ( const guard2tc & g1, const guard2tc & g2 )

friend

operator|=

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

friend

Member Data Documentation

guard_list

guard_seq guard2tc::guard_list

---

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

• src/irep2/irep2_guard.h
• src/irep2/irep2_guard.cpp