diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-10-14 20:03:17 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-10-30 12:22:52 +0000 |
commit | 416f7818aedaf7b6bdd478692871cc46aa724f79 (patch) | |
tree | 5d583de9c4ba1d5df121e9776c3e1147cd257240 /test/CXX/StaticDestructor.cpp | |
parent | eb197d5737fa8fe9e75747ee1a26ee55b942c916 (diff) | |
download | klee-416f7818aedaf7b6bdd478692871cc46aa724f79.tar.gz |
Optimize StaticDestructor test to be less fragile to compiler optimizations.
Diffstat (limited to 'test/CXX/StaticDestructor.cpp')
-rw-r--r-- | test/CXX/StaticDestructor.cpp | 13 |
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); } }; |