aboutsummaryrefslogtreecommitdiffhomepage
path: root/test
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2020-10-14 20:03:17 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2020-10-30 12:22:52 +0000
commit416f7818aedaf7b6bdd478692871cc46aa724f79 (patch)
tree5d583de9c4ba1d5df121e9776c3e1147cd257240 /test
parenteb197d5737fa8fe9e75747ee1a26ee55b942c916 (diff)
downloadklee-416f7818aedaf7b6bdd478692871cc46aa724f79.tar.gz
Optimize StaticDestructor test to be less fragile to compiler optimizations.
Diffstat (limited to 'test')
-rw-r--r--test/CXX/StaticDestructor.cpp13
1 files changed, 5 insertions, 8 deletions
diff --git a/test/CXX/StaticDestructor.cpp b/test/CXX/StaticDestructor.cpp
index 090ae761..172d9f94 100644
--- a/test/CXX/StaticDestructor.cpp
+++ b/test/CXX/StaticDestructor.cpp
@@ -1,21 +1,18 @@
-// don't optimize this, llvm likes to turn the *p into unreachable
-
// RUN: %clangxx %s -emit-llvm -g %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --optimize=false --libc=klee --write-no-tests %t1.bc 2> %t1.log
+// RUN: %klee --output-dir=%t.klee-out --libc=klee %t1.bc 2> %t1.log
// RUN: FileCheck --input-file %t1.log %s
#include <cassert>
class Test {
- int *p;
+ int x;
public:
- Test() : p(0) {}
+ Test() : x(13) {}
~Test() {
- assert(!p);
- // CHECK: :[[@LINE+1]]: memory error
- assert(*p == 10); // crash here
+ // CHECK: :[[@LINE+1]]: divide by zero
+ x = x / (x - 13);
}
};