about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2016-11-19 19:42:27 +0000
committerGitHub <noreply@github.com>2016-11-19 19:42:27 +0000
commit1eed21e1f4c374ea6d90734f4fcf32062438cc8a (patch)
tree52218eed73e5378e36d05e3961adfb94458c28a3 /lib
parent12442a55eaed122a5e10c377f6661831c824063c (diff)
parent3fdd9a903837a6750e42fd6d7ada342def63a7b3 (diff)
downloadklee-1eed21e1f4c374ea6d90734f4fcf32062438cc8a.tar.gz
Merge pull request #492 from hoangmle/master
add nicer error messages for --use-merge and add explanation why it currently cannot be used with random-path
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Searcher.cpp2
-rw-r--r--lib/Core/UserSearcher.cpp8
2 files changed, 8 insertions, 2 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 3bfcd6b3..47f300d1 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -402,6 +402,8 @@ Instruction *MergingSearcher::getMergePoint(ExecutionState &es) {
 }
 
 ExecutionState &MergingSearcher::selectState() {
+  // FIXME: this loop is endless if baseSearcher includes RandomPathSearcher.
+  // The reason is that RandomPathSearcher::removeState() does nothing...
   while (!baseSearcher->empty()) {
     ExecutionState &es = baseSearcher->selectState();
     if (getMergePoint(es)) {
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index fcda26f2..0aa4a4b0 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -117,8 +117,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
 
   // merge support is experimental
   if (UseMerge) {
-    assert(!UseBumpMerge);
-    assert(std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) == CoreSearch.end()); // XXX: needs further debugging: test/Features/Searchers.c fails with this searcher
+    if (UseBumpMerge)
+      klee_error("use-merge and use-bump-merge cannot be used together");
+    // RandomPathSearcher cannot be used in conjunction with MergingSearcher,
+    // see MergingSearcher::selectState() for explanation.
+    if (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::RandomPath) != CoreSearch.end())
+      klee_error("use-merge currently does not support random-path, please use another search strategy");
     searcher = new MergingSearcher(executor, searcher);
   } else if (UseBumpMerge) {
     searcher = new BumpMergingSearcher(executor, searcher);