lib/Core/SeedInfo.h


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

//===-- 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/util/Assignment.h"

extern "C" {
  struct BOut;
  struct BOutObject;
}

namespace klee {
  class ExecutionState;
  class TimingSolver;

  class SeedInfo {
  public:
    Assignment assignment;
    BOut *input;
    unsigned inputPosition;
    std::set<struct BOutObject*> used;
    
  public:
    explicit
    SeedInfo(BOut *_input) : assignment(true),
                             input(_input),
                             inputPosition(0) {}
    
    BOutObject *getNextInput(const MemoryObject *mo,
                             bool byName);
    
    /// Patch the seed so that condition is satisfied while retaining as
    /// many of the seed values as possible.
    void patchSeed(const ExecutionState &state, 
                   ref<Expr> condition,
                   TimingSolver *solver);
  };
}

#endif