Public Attributes | List of all members
Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::NextUnit Struct Reference


Return value for nextUnits.

Definition at line 218 of file SemanticCallbacks.h.

#include <SemanticCallbacks.h>

Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::NextUnit:
Collaboration graph

Public Attributes

ExecutionUnitPtr unit
 Unit to be executed. More...
SymbolicExpr::Ptr assertion
 Path assertion for this unit. More...
SmtSolver::Evidence evidence
 SMT solver evidence that this is a feasible path. More...

Member Data Documentation

ExecutionUnitPtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::NextUnit::unit

Unit to be executed.

Definition at line 219 of file SemanticCallbacks.h.

SymbolicExpr::Ptr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::NextUnit::assertion

Path assertion for this unit.

Definition at line 220 of file SemanticCallbacks.h.

SmtSolver::Evidence Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::NextUnit::evidence

SMT solver evidence that this is a feasible path.

Definition at line 221 of file SemanticCallbacks.h.

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