blob: 60a4fb51419c470aaf523d3fbebc4cc272471040 (
plain) (
blame)
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
//===-- DummySolver.cpp ---------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "klee/Solver/Solver.h"
#include "klee/Solver/SolverImpl.h"
#include "klee/Solver/SolverStats.h"
namespace klee {
class DummySolverImpl : public SolverImpl {
public:
DummySolverImpl();
bool computeValidity(const Query &, Solver::Validity &result);
bool computeTruth(const Query &, bool &isValid);
bool computeValue(const Query &, ref<Expr> &result);
bool computeInitialValues(const Query &,
const std::vector<const Array *> &objects,
std::vector<std::vector<unsigned char> > &values,
bool &hasSolution);
SolverRunStatus getOperationStatusCode();
};
DummySolverImpl::DummySolverImpl() {}
bool DummySolverImpl::computeValidity(const Query &, Solver::Validity &result) {
++stats::queries;
// FIXME: We should have stats::queriesFail;
return false;
}
bool DummySolverImpl::computeTruth(const Query &, bool &isValid) {
++stats::queries;
// FIXME: We should have stats::queriesFail;
return false;
}
bool DummySolverImpl::computeValue(const Query &, ref<Expr> &result) {
++stats::queries;
++stats::queryCounterexamples;
return false;
}
bool DummySolverImpl::computeInitialValues(
const Query &, const std::vector<const Array *> &objects,
std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
++stats::queries;
++stats::queryCounterexamples;
return false;
}
SolverImpl::SolverRunStatus DummySolverImpl::getOperationStatusCode() {
return SOLVER_RUN_STATUS_FAILURE;
}
Solver *createDummySolver() { return new Solver(new DummySolverImpl()); }
}
|
