about summary refs log tree commit diff homepage
path: root/test/CXX
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/CXX
parenteb197d5737fa8fe9e75747ee1a26ee55b942c916 (diff)
downloadklee-416f7818aedaf7b6bdd478692871cc46aa724f79.tar.gz
Optimize StaticDestructor test to be less fragile to compiler optimizations.
Diffstat (limited to 'test/CXX')
-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);
   }
 };