about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-04-01 14:11:23 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-07-01 15:52:40 +0100
commitfdfc73bb3217c3a9527e09075b52aecdf19de666 (patch)
tree617ec2bcdb26627d123daf27f2fbabf0add70a25 /lib
parent8a0f1af7500e10dadd97300f242424917d2e9902 (diff)
downloadklee-fdfc73bb3217c3a9527e09075b52aecdf19de666.tar.gz
Remove state contructor with constraints
This constructor has been a hack and was wrongly used, use ConstraintManager instead.
Allow copy-constructing states only via `ExecutionState::branch()` call.
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/ExecutionState.cpp3
-rw-r--r--lib/Core/ExecutionState.h13
2 files changed, 8 insertions, 8 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 5e95ca9b..5dfabe9e 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -82,9 +82,6 @@ ExecutionState::ExecutionState(KFunction *kf) :
   setID();
 }
 
-ExecutionState::ExecutionState(const std::vector<ref<Expr>> &assumptions)
-    : constraints(assumptions), ptreeNode(nullptr) {}
-
 ExecutionState::~ExecutionState() {
   for (const auto &cur_mergehandler: openMergeStack){
     cur_mergehandler->removeOpenState(this);
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index 03cad916..7be69ea7 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -65,6 +65,14 @@ struct StackFrame {
 
 /// @brief ExecutionState representing a path under exploration
 class ExecutionState {
+#ifdef KLEE_UNITTEST
+public:
+#else
+private:
+#endif
+  // copy ctor
+  ExecutionState(const ExecutionState &state);
+
 public:
   using stack_ty = std::vector<StackFrame>;
 
@@ -152,11 +160,6 @@ public:
   #endif
   // only to create the initial state
   explicit ExecutionState(KFunction *kf);
-  // XXX total hack, just used to make a state so solver can
-  // use on structure
-  explicit ExecutionState(const std::vector<ref<Expr>> &assumptions);
-  // copy ctor
-  ExecutionState(const ExecutionState &state);
   // no copy assignment, use copy constructor
   ExecutionState &operator=(const ExecutionState &) = delete;
   // no move ctor