ROSE  0.9.10.205
Public Member Functions | List of all members
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 one level from the solver unless this object is in the isCommitted state (see commit). This guard object makes no attempt to ensure that the level popped is the same as the one that was initially pushed by the constructor.

Definition at line 111 of file BinarySmtSolver.h.

#include <BinarySmtSolver.h>

Public Member Functions

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

Constructor & Destructor Documentation

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 118 of file BinarySmtSolver.h.

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

Destructor pops level unless canceled.

Definition at line 125 of file BinarySmtSolver.h.

Member Function Documentation

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

Cancel the popping during the destructor.

Definition at line 136 of file BinarySmtSolver.h.

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

Whether the guard is canceled.

Definition at line 141 of file BinarySmtSolver.h.

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

Solver being protected.

Definition at line 146 of file BinarySmtSolver.h.


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