about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2018-05-15 13:55:28 +0100
committerMartinNowack <martin.nowack@gmail.com>2018-05-15 15:18:08 +0100
commit0cf0150da0f674c85f9eaccee8b487ed004c3edc (patch)
tree91e4f85c2e1c1c09d3e1ab852c6473241d44d638
parentdc610f616940823e9cd8511cd10ca05721b53caf (diff)
downloadklee-0cf0150da0f674c85f9eaccee8b487ed004c3edc.tar.gz
remove QueryLog.h
-rw-r--r--include/klee/Internal/Support/QueryLog.h63
-rw-r--r--lib/Solver/KQueryLoggingSolver.cpp1
2 files changed, 0 insertions, 64 deletions
diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h
deleted file mode 100644
index 212ab760..00000000
--- a/include/klee/Internal/Support/QueryLog.h
+++ /dev/null
@@ -1,63 +0,0 @@
-//===-- QueryLog.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_OPT_LOGGINGSOLVER_H
-#define KLEE_OPT_LOGGINGSOLVER_H
-
-#include "klee/Expr.h"
-
-#include <vector>
-
-namespace klee {
-  struct Query;
-
-  class QueryLogEntry {
-  public:
-    enum Type {
-      Validity,
-      Truth,
-      Value,
-      Cex
-    };
-    
-    typedef std::vector< ref<Expr> > exprs_ty;
-    exprs_ty exprs;
-
-    Type type;
-    ref<Expr> query;
-    unsigned instruction;
-    std::vector<const Array*> objects;
-    
-  public:
-    QueryLogEntry() : query(ConstantExpr::alloc(0,Expr::Bool)) {}
-    QueryLogEntry(const QueryLogEntry &b);
-    QueryLogEntry(const Query &_query, 
-                  Type _type,
-                  const std::vector<const Array*> *objects = 0);
-  };
-
-  class QueryLogResult {
-  public:
-    uint64_t result;
-    double time;
-
-  public:
-    QueryLogResult() {}
-    QueryLogResult(bool _success, uint64_t _result, double _time) 
-      : result(_result), time(_time) {
-      if (!_success) { // la la la
-        result = 0;
-        time = -1;
-      }
-    }
-  };
-  
-}
-
-#endif
diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
index a0ac950c..8dc98ac5 100644
--- a/lib/Solver/KQueryLoggingSolver.cpp
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -11,7 +11,6 @@
 
 #include "klee/Expr.h"
 #include "klee/util/ExprPPrinter.h"
-#include "klee/Internal/Support/QueryLog.h"
 
 using namespace klee;