Rose::BinaryAnalysis::SmtSolver::Transaction Class Reference

Description

RAII guard for solver stack.

This object implements a rudimentary form of SMT transactions. The constructor starts a new transaction by pushing a new level onto the specified solver (if the solver is non-null). The destructor pops transactions until it gets back to the same number of levels as originally. It is undefined behavior if the solver has fewer transactions than originally when the destructor is called. If commit has been called on this object then the destructor does nothing.

This guard object makes no attempt to ensure that after popping levels we end up at the same level we started at. In other words, although the number of levels is back to where we started, it might have been possible that between the constructor and destructor we popped past this transaction and then pushed new transactions to replace it with a different transaction.

Definition at line 133 of file SmtSolver.h.

#include <Rose/BinaryAnalysis/SmtSolver.h>

Public Member Functions
	Transaction (const SmtSolver::Ptr &solver)
	Constructor pushes level if solver is non-null.
	~Transaction ()
	Destructor pops level unless canceled.
void	commit (bool b=true)
	Cancel the popping during the destructor.
bool	isCommitted () const
	Whether the guard is canceled.
SmtSolver::Ptr	solver () const
	Solver being protected.

Constructor & Destructor Documentation

Transaction()

Rose::BinaryAnalysis::SmtSolver::Transaction::Transaction ( const SmtSolver::Ptr &  solver )

inlineexplicit

Constructor pushes level if solver is non-null.

It is safe to call this with a null solver.

Definition at line 141 of file SmtSolver.h.

References solver().

~Transaction()

Rose::BinaryAnalysis::SmtSolver::Transaction::~Transaction ( )

inline

Destructor pops level unless canceled.

Definition at line 152 of file SmtSolver.h.

Member Function Documentation

commit()

void Rose::BinaryAnalysis::SmtSolver::Transaction::commit ( bool  b = true )

inline

Cancel the popping during the destructor.

Definition at line 166 of file SmtSolver.h.

isCommitted()

bool Rose::BinaryAnalysis::SmtSolver::Transaction::isCommitted ( ) const

inline

Whether the guard is canceled.

Definition at line 171 of file SmtSolver.h.

solver()

SmtSolver::Ptr Rose::BinaryAnalysis::SmtSolver::Transaction::solver ( ) const

inline

Solver being protected.

Definition at line 176 of file SmtSolver.h.

Referenced by Transaction().

---

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

• SmtSolver.h