summaryrefslogtreecommitdiff
path: root/klee
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2012-09-12 14:37:39 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2012-09-12 14:37:39 +0000
commit86d0170ae8bcbfbe1708b7d99f2d706f13cff463 (patch)
tree9de92af88741a431aaafb24d259b3c5054d904aa /klee
parent21c60ba9a9ff6bfcc8061b3d7a47e281dd79e3cc (diff)
Restructured the command-line options for setting the search
heuristics in KLEE. The new options are documented at http://klee.llvm.org/klee-options.html. Cleaned a bit the code in UserSearcher.cpp, and fixed some test cases to use the new options.
Diffstat (limited to 'klee')
-rw-r--r--klee/lib/Core/Searcher.h12
-rw-r--r--klee/lib/Core/UserSearcher.cpp158
-rw-r--r--klee/lib/Core/UserSearcher.h2
-rw-r--r--klee/test/Dogfood/ImmutableSet.cpp2
-rw-r--r--klee/test/Feature/CopyOnWrite.c2
-rw-r--r--klee/test/Feature/MakeSymbolicName.c2
-rw-r--r--klee/test/Feature/Searchers.c31
-rw-r--r--klee/test/Runtime/POSIX/DirConsistency.c4
-rw-r--r--klee/test/Runtime/POSIX/FD_Fail2.c15
-rw-r--r--klee/www/Documentation.html5
-rw-r--r--klee/www/klee-options.html73
11 files changed, 181 insertions, 125 deletions
diff --git a/klee/lib/Core/Searcher.h b/klee/lib/Core/Searcher.h
index 9703e97391d..58772bbb51f 100644
--- a/klee/lib/Core/Searcher.h
+++ b/klee/lib/Core/Searcher.h
@@ -66,6 +66,18 @@ namespace klee {
tmp.insert(es);
update(current, std::set<ExecutionState*>(), tmp);
}
+
+ enum CoreSearchType {
+ DFS,
+ RandomState,
+ RandomPath,
+ NURS_CovNew,
+ NURS_MD2U,
+ NURS_Depth,
+ NURS_ICnt,
+ NURS_CPICnt,
+ NURS_QC
+ };
};
class DFSSearcher : public Searcher {
diff --git a/klee/lib/Core/UserSearcher.cpp b/klee/lib/Core/UserSearcher.cpp
index 1aff9e5e8d6..361092d2b68 100644
--- a/klee/lib/Core/UserSearcher.cpp
+++ b/klee/lib/Core/UserSearcher.cpp
@@ -20,61 +20,27 @@ using namespace llvm;
using namespace klee;
namespace {
- cl::opt<bool>
- UseRandomSearch("use-random-search");
-
- cl::opt<bool>
- UseInterleavedRS("use-interleaved-RS");
-
- cl::opt<bool>
- UseInterleavedNURS("use-interleaved-NURS");
-
- cl::opt<bool>
- UseInterleavedMD2UNURS("use-interleaved-MD2U-NURS");
-
- cl::opt<bool>
- UseInterleavedInstCountNURS("use-interleaved-icnt-NURS");
-
- cl::opt<bool>
- UseInterleavedCPInstCountNURS("use-interleaved-cpicnt-NURS");
-
- cl::opt<bool>
- UseInterleavedQueryCostNURS("use-interleaved-query-cost-NURS");
+ cl::list<Searcher::CoreSearchType>
+ CoreSearch("search", cl::desc("Specify the search heuristic (default=random-path interleaved with nurs:covnew)"),
+ cl::values(clEnumValN(Searcher::DFS, "dfs", "use Depth First Search (DFS)"),
+ clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"),
+ clEnumValN(Searcher::RandomPath, "random-path", "use Random Path Selection (see OSDI'08 paper)"),
+ clEnumValN(Searcher::NURS_CovNew, "nurs:covnew", "use Non Uniform Random Search (NURS) with Coverage-New"),
+ clEnumValN(Searcher::NURS_MD2U, "nurs:md2u", "use NURS with Min-Dist-to-Uncovered"),
+ clEnumValN(Searcher::NURS_Depth, "nurs:depth", "use NURS with 2^depth"),
+ clEnumValN(Searcher::NURS_ICnt, "nurs:icnt", "use NURS with Instr-Count"),
+ clEnumValN(Searcher::NURS_CPICnt, "nurs:cpicnt", "use NURS with CallPath-Instr-Count"),
+ clEnumValN(Searcher::NURS_QC, "nurs:qc", "use NURS with Query-Cost"),
+ clEnumValEnd));
cl::opt<bool>
- UseInterleavedCovNewNURS("use-interleaved-covnew-NURS");
-
- cl::opt<bool>
- UseNonUniformRandomSearch("use-non-uniform-random-search");
-
- cl::opt<bool>
- UseRandomPathSearch("use-random-path");
-
- cl::opt<WeightedRandomSearcher::WeightType>
- WeightType("weight-type", cl::desc("Set the weight type for --use-non-uniform-random-search"),
- cl::values(clEnumValN(WeightedRandomSearcher::Depth, "none", "use (2^depth)"),
- clEnumValN(WeightedRandomSearcher::InstCount, "icnt", "use current pc exec count"),
- clEnumValN(WeightedRandomSearcher::CPInstCount, "cpicnt", "use current pc exec count"),
- clEnumValN(WeightedRandomSearcher::QueryCost, "query-cost", "use query cost"),
- clEnumValN(WeightedRandomSearcher::MinDistToUncovered, "md2u", "use min dist to uncovered"),
- clEnumValN(WeightedRandomSearcher::CoveringNew, "covnew", "use min dist to uncovered + coveringNew flag"),
- clEnumValEnd));
-
- cl::opt<bool>
- UseMerge("use-merge",
- cl::desc("Enable support for klee_merge() (experimental)"));
-
- cl::opt<bool>
- UseBumpMerge("use-bump-merge",
- cl::desc("Enable support for klee_merge() (extra experimental)"));
-
- cl::opt<bool>
UseIterativeDeepeningTimeSearch("use-iterative-deepening-time-search",
cl::desc("(experimental)"));
cl::opt<bool>
UseBatchingSearch("use-batching-search",
- cl::desc("Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time"));
+ cl::desc("Use batching searcher (keep running selected state for N instructions/time, see --batch-instructions and --batch-time)"),
+ cl::init(false));
cl::opt<unsigned>
BatchInstructions("batch-instructions",
@@ -85,68 +51,62 @@ namespace {
BatchTime("batch-time",
cl::desc("Amount of time to batch when using --use-batching-search"),
cl::init(5.0));
+
+
+ cl::opt<bool>
+ UseMerge("use-merge",
+ cl::desc("Enable support for klee_merge() (experimental)"));
+
+ cl::opt<bool>
+ UseBumpMerge("use-bump-merge",
+ cl::desc("Enable support for klee_merge() (extra experimental)"));
+
}
+
bool klee::userSearcherRequiresMD2U() {
- return (WeightType==WeightedRandomSearcher::MinDistToUncovered ||
- WeightType==WeightedRandomSearcher::CoveringNew ||
- UseInterleavedMD2UNURS ||
- UseInterleavedCovNewNURS ||
- UseInterleavedInstCountNURS ||
- UseInterleavedCPInstCountNURS ||
- UseInterleavedQueryCostNURS);
+ return (std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_MD2U) != CoreSearch.end() ||
+ std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_CovNew) != CoreSearch.end() ||
+ std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_ICnt) != CoreSearch.end() ||
+ std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_CPICnt) != CoreSearch.end() ||
+ std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
}
-// FIXME: Remove.
-bool klee::userSearcherRequiresBranchSequences() {
- return false;
+
+Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
+ Searcher *searcher = NULL;
+ switch (type) {
+ case Searcher::DFS: searcher = new DFSSearcher(); break;
+ case Searcher::RandomState: searcher = new RandomSearcher(); break;
+ case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
+ case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
+ case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::MinDistToUncovered); break;
+ case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::Depth); break;
+ case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::InstCount); break;
+ case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CPInstCount); break;
+ case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::QueryCost); break;
+ }
+
+ return searcher;
}
Searcher *klee::constructUserSearcher(Executor &executor) {
- Searcher *searcher = 0;
-
- if (UseRandomPathSearch) {
- searcher = new RandomPathSearcher(executor);
- } else if (UseNonUniformRandomSearch) {
- searcher = new WeightedRandomSearcher(executor, WeightType);
- } else if (UseRandomSearch) {
- searcher = new RandomSearcher();
- } else {
- searcher = new DFSSearcher();
+
+ // default values
+ if (CoreSearch.size() == 0) {
+ CoreSearch.push_back(Searcher::RandomPath);
+ CoreSearch.push_back(Searcher::NURS_CovNew);
}
- if (UseInterleavedNURS || UseInterleavedMD2UNURS || UseInterleavedRS ||
- UseInterleavedCovNewNURS || UseInterleavedInstCountNURS ||
- UseInterleavedCPInstCountNURS || UseInterleavedQueryCostNURS) {
+ Searcher *searcher = getNewSearcher(CoreSearch[0], executor);
+
+ if (CoreSearch.size() > 1) {
std::vector<Searcher *> s;
s.push_back(searcher);
-
- if (UseInterleavedNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::Depth));
- if (UseInterleavedMD2UNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::MinDistToUncovered));
-
- if (UseInterleavedCovNewNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::CoveringNew));
-
- if (UseInterleavedInstCountNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::InstCount));
-
- if (UseInterleavedCPInstCountNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::CPInstCount));
-
- if (UseInterleavedQueryCostNURS)
- s.push_back(new WeightedRandomSearcher(executor,
- WeightedRandomSearcher::QueryCost));
-
- if (UseInterleavedRS)
- s.push_back(new RandomSearcher());
+ for (unsigned i=1; i<CoreSearch.size(); i++)
+ s.push_back(getNewSearcher(CoreSearch[i], executor));
+
searcher = new InterleavedSearcher(s);
}
@@ -154,10 +114,12 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
}
+ // 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
searcher = new MergingSearcher(executor, searcher);
- } else if (UseBumpMerge) {
+ } else if (UseBumpMerge) {
searcher = new BumpMergingSearcher(executor, searcher);
}
diff --git a/klee/lib/Core/UserSearcher.h b/klee/lib/Core/UserSearcher.h
index 9571bf5b400..d01a017f4ef 100644
--- a/klee/lib/Core/UserSearcher.h
+++ b/klee/lib/Core/UserSearcher.h
@@ -17,8 +17,6 @@ namespace klee {
// XXX gross, should be on demand?
bool userSearcherRequiresMD2U();
- bool userSearcherRequiresBranchSequences();
-
Searcher *constructUserSearcher(Executor &executor);
}
diff --git a/klee/test/Dogfood/ImmutableSet.cpp b/klee/test/Dogfood/ImmutableSet.cpp
index bdb9f431c68..95320a82f5a 100644
--- a/klee/test/Dogfood/ImmutableSet.cpp
+++ b/klee/test/Dogfood/ImmutableSet.cpp
@@ -1,5 +1,5 @@
// RUN: %llvmgxx -I../../../include -g -DMAX_ELEMENTS=4 -fno-exceptions -emit-llvm -c -o %t1.bc %s
-// RUN: %klee --libc=klee --max-forks=200 --no-output --exit-on-error --optimize --disable-inlining --use-non-uniform-random-search --use-cex-cache %t1.bc
+// RUN: %klee --libc=klee --max-forks=200 --no-output --exit-on-error --optimize --disable-inlining --search=nurs:depth --use-cex-cache %t1.bc
#include "klee/klee.h"
#include "klee/Internal/ADT/ImmutableSet.h"
diff --git a/klee/test/Feature/CopyOnWrite.c b/klee/test/Feature/CopyOnWrite.c
index ee3ea15e7d7..ce77c802432 100644
--- a/klee/test/Feature/CopyOnWrite.c
+++ b/klee/test/Feature/CopyOnWrite.c
@@ -1,5 +1,5 @@
// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
#include <assert.h>
diff --git a/klee/test/Feature/MakeSymbolicName.c b/klee/test/Feature/MakeSymbolicName.c
index a4d4e2a68db..a31b4a9b8d2 100644
--- a/klee/test/Feature/MakeSymbolicName.c
+++ b/klee/test/Feature/MakeSymbolicName.c
@@ -1,5 +1,5 @@
// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
-// RUN: %klee --use-random-search --exit-on-error %t1.bc
+// RUN: %klee --search=random-state --exit-on-error %t1.bc
#include <assert.h>
diff --git a/klee/test/Feature/Searchers.c b/klee/test/Feature/Searchers.c
index d61037b9266..b120d354578 100644
--- a/klee/test/Feature/Searchers.c
+++ b/klee/test/Feature/Searchers.c
@@ -1,27 +1,30 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %klee %t2.bc
-// RUN: %klee --use-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --search=random-state %t2.bc
+// RUN: %klee --search=nurs:depth %t2.bc
+// RUN: %klee --search=nurs:qc %t2.bc
// RUN: %klee --use-batching-search %t2.bc
-// RUN: %klee --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
-// RUN: %klee --use-merge --debug-log-merge --debug-log-state-merge %t2.bc
-// RUN: %klee --use-merge --use-batching-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-batching-search --search=nurs:qc %t2.bc
+// RUN: %klee --search=random-path --search=nurs:qc %t2.bc
+// RUN: %klee --use-merge --search=dfs --debug-log-merge --debug-log-state-merge %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=dfs %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-merge --use-batching-search --search=nurs:qc %t2.bc
// RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search %t2.bc
-// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=random-state %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:depth %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --search=nurs:qc %t2.bc
/* this test is basically just for coverage and doesn't really do any
correctness check (aside from testing that the various combinations
don't crash) */
+#include <stdlib.h>
+
int validate(char *buf, int N) {
int i;
diff --git a/klee/test/Runtime/POSIX/DirConsistency.c b/klee/test/Runtime/POSIX/DirConsistency.c
index 30696650102..24bb8a6e9b5 100644
--- a/klee/test/Runtime/POSIX/DirConsistency.c
+++ b/klee/test/Runtime/POSIX/DirConsistency.c
@@ -1,7 +1,7 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
+// RUN: %klee --run-in=/tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
// RUN: %llvmgcc -D_FILE_OFFSET_BITS=64 %s -emit-llvm -O0 -c -o %t.bc
-// RUN: %klee --run-in=/tmp --use-random-search --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
+// RUN: %klee --run-in=/tmp --search=random-state --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
// RUN: sort %t1.log %t2.log | uniq -c > %t3.log
// RUN: grep -q "4 COUNT" %t3.log
diff --git a/klee/test/Runtime/POSIX/FD_Fail2.c b/klee/test/Runtime/POSIX/FD_Fail2.c
index 062f7027006..b42e03bfea3 100644
--- a/klee/test/Runtime/POSIX/FD_Fail2.c
+++ b/klee/test/Runtime/POSIX/FD_Fail2.c
@@ -1,5 +1,5 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --libc=uclibc --posix-runtime %t1.bc --sym-files 0 0 --max-fail 1
+// RUN: %klee --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 1
// RUN: test -f klee-last/test000001.ktest
// RUN: test -f klee-last/test000002.ktest
// RUN: test -f klee-last/test000003.ktest
@@ -14,21 +14,24 @@
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
+#include <stdio.h>
int main(int argc, char** argv) {
char buf[1024];
- int fd = open("/etc/fstab", O_RDONLY);
+ int fd = open("A", O_RDONLY);
assert(fd != -1);
-
- int r = read(fd, buf, 1, 100);
+
+ int r;
+
+ r = read(fd, buf, 1, 5);
if (r != -1)
printf("read() succeeded\n");
- else printf("read() failed with errno %s\n", strerror(errno));
+ else printf("read() failed with error '%s'\n", strerror(errno));
r = close(fd);
if (r != -1)
printf("close() succeeded\n");
- else printf("close() failed with errno %s\n", strerror(errno));
+ else printf("close() failed with error '%s'\n", strerror(errno));
return 0;
}
diff --git a/klee/www/Documentation.html b/klee/www/Documentation.html
index cf20cc5d949..b266e439c07 100644
--- a/klee/www/Documentation.html
+++ b/klee/www/Documentation.html
@@ -23,6 +23,11 @@
</li>
<li>
+ <a href="klee-options.html">KLEE Options</a>:
+ Overview of the KLEE's main command-line options.
+ </li>
+
+ <li>
<a href="klee-files.html">KLEE Generated Files</a>:
Overview of the main files generated by KLEE.
diff --git a/klee/www/klee-options.html b/klee/www/klee-options.html
new file mode 100644
index 00000000000..22871e0e76a
--- /dev/null
+++ b/klee/www/klee-options.html
@@ -0,0 +1,73 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
+ "http://www.w3.org/TR/html4/strict.dtd">
+<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ -->
+<html>
+<head>
+ <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
+ <title>The KLEE Symbolic Virtual Machine</title>
+ <link type="text/css" rel="stylesheet" href="menu.css">
+ <link type="text/css" rel="stylesheet" href="content.css">
+</head>
+<body>
+<!--#include virtual="menu.html.incl"-->
+<div id="content">
+ <!--*********************************************************************-->
+ <h1>KLEE Options</h1>
+ <!--*********************************************************************-->
+
+ <h2>Search Heuristics</h2>
+
+ <h3>Main search heuristics</h3>
+
+ <p>
+ KLEE provides four main search heuristics:
+ <ol>
+ <li><b>Depth-First Search (DFS):</b> Traverses states in depth-first order.</li>
+ <li><b>Random State Search:</b>Randomly selects a state to explore.</li>
+ <li><b>Random Path Selection:</b> Described in our <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">KLEE OSDI'08</a> paper.</li>
+ <li><b>Non Uniform Random Search (NURS):</b> Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc.
+ </ol>
+
+ To select a search heuristic, use the <b>--search</b> option provided by KLEE. For example:
+ <pre class="output">
+ $ klee --search=dfs demo.o</pre>
+
+ runs <i>demo.o</i> using DFS, while
+ <pre class="output">
+ $ klee --search=random-path demo.o </pre>
+ runs it using the random path selection strategy.
+
+ The full list of options is shown in KLEE's help message:
+ <pre class="output">
+ $ klee --help
+ -search - Specify the search heuristic (default=random-path interleaved with nurs:covnew)
+ =dfs - use Depth First Search (DFS)
+ =random-state - randomly select a state to explore
+ =random-path - use Random Path Selection (see OSDI'08 paper)
+ =nurs:covnew - use Non Uniform Random Search (NURS) with Coverage-New heuristic
+ =nurs:md2u - use NURS with Min-Dist-to-Uncovered heuristic
+ =nurs:depth - use NURS with 2^depth heuristic
+ =nurs:icnt - use NURS with Instr-Count heuristic
+ =nurs:cpicnt - use NURS with CallPath-Instr-Count heuristic
+ =nurs:qc - use NURS with Query-Cost heuristic </pre>
+
+
+ <h3>Interleaving search heuristics</h3>
+ <p>
+ Search heuristics in KLEE can be interleaved in a round-robin
+ fashion. To interleave several search heuristics to be interleaved, use the <b>--search</b> multiple times. For example:
+ <pre class="output">
+ $ klee --search=random-state --search=nurs:md2u demo.o </pre>
+ interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion.
+ <br/>
+ </p>
+
+
+ <h3>Default search heuristics</h3>
+ <p>
+ The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>.
+ </p>
+
+</div>
+</body>
+</html>