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

Description

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
[legend]

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: