SeedInfo.h

Go to the documentation of this file.

//===-- SeedInfo.h ----------------------------------------------*- C++ -*-===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
 
#ifndef KLEE_SEEDINFO_H
#define KLEE_SEEDINFO_H
 
#include "klee/Expr/Assignment.h"
 
extern "C" {
  struct KTest;
  struct KTestObject;
}
 
namespace klee {
  class ExecutionState;
  class TimingSolver;
  class MemoryObject;
 
  class SeedInfo {
  public:
    Assignment assignment;
    KTest *input;
    unsigned inputPosition;
    std::set<struct KTestObject*> used;
    
  public:
    explicit
    SeedInfo(KTest *_input) : assignment(true),
                             input(_input),
                             inputPosition(0) {}
    
    KTestObject *getNextInput(const MemoryObject *mo,
                             bool byName);
    
    void patchSeed(const ExecutionState &state, 
                   ref<Expr> condition,
                   TimingSolver *solver);
  };
}
 
#endif /* KLEE_SEEDINFO_H */