klee
Public Member Functions | Public Attributes | List of all members
klee::SeedInfo Class Reference

#include <SeedInfo.h>

Collaboration diagram for klee::SeedInfo:
Collaboration graph
[legend]

Public Member Functions

 SeedInfo (KTest *_input)
 
KTestObject * getNextInput (const MemoryObject *mo, bool byName)
 
void patchSeed (const ExecutionState &state, ref< Expr > condition, TimingSolver *solver)
 

Public Attributes

Assignment assignment
 
KTest * input
 
unsigned inputPosition
 
std::set< struct KTestObject * > used
 

Detailed Description

Definition at line 25 of file SeedInfo.h.

Constructor & Destructor Documentation

◆ SeedInfo()

klee::SeedInfo::SeedInfo ( KTest *  _input)
inlineexplicit

Definition at line 34 of file SeedInfo.h.

Member Function Documentation

◆ getNextInput()

KTestObject * SeedInfo::getNextInput ( const MemoryObject *  mo,
bool  byName 
)

Definition at line 24 of file SeedInfo.cpp.

References input, inputPosition, klee::klee_warning_once(), KTestObject::name, klee::MemoryObject::name, KTestObject::numBytes, KTest::numObjects, KTest::objects, klee::MemoryObject::size, and used.

Referenced by klee::Executor::executeMakeSymbolic().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ patchSeed()

void SeedInfo::patchSeed ( const ExecutionState &  state,
ref< Expr >  condition,
TimingSolver *  solver 
)

Patch the seed so that condition is satisfied while retaining as many of the seed values as possible.

Definition at line 62 of file SeedInfo.cpp.

References klee::ConstraintManager::addConstraint(), klee::ConstantExpr::alloc(), assignment, klee::Assignment::bindings, klee::ExecutionState::constraints, klee::ReadExpr::create(), klee::Assignment::evaluate(), klee::findReads(), klee::TimingSolver::getValue(), klee::ReadExpr::index, klee::Expr::Int32, klee::Expr::Int8, klee::TimingSolver::mayBeTrue(), klee::TimingSolver::mustBeFalse(), klee::ExecutionState::queryMetaData, klee::UpdateList::root, klee::Array::size, and klee::ReadExpr::updates.

Here is the call graph for this function:

Member Data Documentation

◆ assignment

Assignment klee::SeedInfo::assignment

Definition at line 27 of file SeedInfo.h.

Referenced by klee::Executor::executeMakeSymbolic(), and patchSeed().

◆ input

KTest* klee::SeedInfo::input

Definition at line 28 of file SeedInfo.h.

Referenced by getNextInput().

◆ inputPosition

unsigned klee::SeedInfo::inputPosition

Definition at line 29 of file SeedInfo.h.

Referenced by getNextInput().

◆ used

std::set<struct KTestObject*> klee::SeedInfo::used

Definition at line 30 of file SeedInfo.h.

Referenced by getNextInput().

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