From 2b2b2b0e46ae260e7974f0d2738f2d23ca255874 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 9 Nov 2016 22:51:48 +0100 Subject: Fix BFS searcher For performance reasons, if KLEE branches, one state is reused and it is progressed by adding new constraints. Make sure both new states end up at the end of the BFS searcher queue. --- test/Feature/BFSSearcher.c | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test/Feature/BFSSearcher.c (limited to 'test') diff --git a/test/Feature/BFSSearcher.c b/test/Feature/BFSSearcher.c new file mode 100644 index 00000000..313791d5 --- /dev/null +++ b/test/Feature/BFSSearcher.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=500 --search=bfs %t1.bc 2>%t2.log +// RUN: FileCheck -input-file=%t2.log %s +#include "assert.h" +#include "klee/klee.h" + +int nd() { + int r; + klee_make_symbolic(&r, sizeof(r), "r"); + return r; +} + +int main() { + int x = 1; + while (nd() != 0) { + x *= 2; + } + // CHECK: ASSERTION FAIL + klee_assert(0); + return x; +} -- cgit 1.4.1