diff options
author | Frank Busse <bb0xfb@gmail.com> | 2023-03-24 21:14:02 +0000 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-12 12:00:35 +0000 |
commit | 19b6ae578b0658115d15848604a28434845bb3e3 (patch) | |
tree | 31d52545929760ad725385bd1cdc1153b710fc75 /unittests/Searcher/SearcherTest.cpp | |
parent | fc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff) | |
download | klee-19b6ae578b0658115d15848604a28434845bb3e3.tar.gz |
new: persistent ptree (-write-ptree) and klee-ptree
Introduce three different kinds of process trees: 1. Noop: does nothing (e.g. no allocations for DFS) 2. InMemory: same behaviour as before (e.g. RandomPathSearcher) 3. Persistent: similar to InMemory but writes nodes to ptree.db and tracks information such as branch type, termination type or source location (asm) in nodes. Enabled with -write-ptree ptree.db files can be analysed/plotted with the new "klee-ptree" tool.
Diffstat (limited to 'unittests/Searcher/SearcherTest.cpp')
-rw-r--r-- | unittests/Searcher/SearcherTest.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp index 0a7c8797..fc0d30ac 100644 --- a/unittests/Searcher/SearcherTest.cpp +++ b/unittests/Searcher/SearcherTest.cpp @@ -24,11 +24,11 @@ namespace { TEST(SearcherTest, RandomPath) { // First state ExecutionState es; - PTree processTree(&es); + InMemoryPTree processTree(es); es.ptreeNode = processTree.root.getPointer(); RNG rng; - RandomPathSearcher rp(processTree, rng); + RandomPathSearcher rp(&processTree, rng); EXPECT_TRUE(rp.empty()); rp.update(nullptr, {&es}, {}); @@ -64,15 +64,15 @@ TEST(SearcherTest, RandomPath) { TEST(SearcherTest, TwoRandomPath) { // Root state ExecutionState root; - PTree processTree(&root); + InMemoryPTree processTree(root); root.ptreeNode = processTree.root.getPointer(); ExecutionState es(root); processTree.attach(root.ptreeNode, &es, &root, BranchType::NONE); RNG rng, rng1; - RandomPathSearcher rp(processTree, rng); - RandomPathSearcher rp1(processTree, rng1); + RandomPathSearcher rp(&processTree, rng); + RandomPathSearcher rp1(&processTree, rng1); EXPECT_TRUE(rp.empty()); EXPECT_TRUE(rp1.empty()); @@ -122,7 +122,7 @@ TEST(SearcherTest, TwoRandomPathDot) { // Root state ExecutionState root; - PTree processTree(&root); + InMemoryPTree processTree(root); root.ptreeNode = processTree.root.getPointer(); rootPNode = root.ptreeNode; @@ -132,8 +132,8 @@ TEST(SearcherTest, TwoRandomPathDot) { esParentPNode = es.ptreeNode; RNG rng; - RandomPathSearcher rp(processTree, rng); - RandomPathSearcher rp1(processTree, rng); + RandomPathSearcher rp(&processTree, rng); + RandomPathSearcher rp1(&processTree, rng); rp.update(nullptr, {&es}, {}); @@ -204,14 +204,14 @@ TEST(SearcherTest, TwoRandomPathDot) { TEST(SearcherDeathTest, TooManyRandomPaths) { // First state ExecutionState es; - PTree processTree(&es); + InMemoryPTree processTree(es); es.ptreeNode = processTree.root.getPointer(); processTree.remove(es.ptreeNode); // Need to remove to avoid leaks RNG rng; - RandomPathSearcher rp(processTree, rng); - RandomPathSearcher rp1(processTree, rng); - RandomPathSearcher rp2(processTree, rng); - ASSERT_DEATH({ RandomPathSearcher rp3(processTree, rng); }, ""); + RandomPathSearcher rp(&processTree, rng); + RandomPathSearcher rp1(&processTree, rng); + RandomPathSearcher rp2(&processTree, rng); + ASSERT_DEATH({ RandomPathSearcher rp3(&processTree, rng); }, ""); } } |