about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-03-13 13:28:48 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-03-17 15:43:21 +0000
commitae6da669e546d2ac0881da2c898c01f28b7ed7e2 (patch)
tree0cc60b6bb5f407a7641a489be640174961221707
parent7ad366f363d23b0aea788fca69349e50180f5f78 (diff)
downloadklee-ae6da669e546d2ac0881da2c898c01f28b7ed7e2.tar.gz
Fix libc++ testcases
* remove wrapper script invocation and script
* add build instruction to test cases
* added additional checks
* add check to avoid execution of tests if KLEE is not compiled with
libc++
-rw-r--r--test/CXX/symex/libc++/atexit.cpp5
-rw-r--r--test/CXX/symex/libc++/compile_with_libcxx.sh15
-rw-r--r--test/CXX/symex/libc++/cout.cpp8
-rw-r--r--test/CXX/symex/libc++/cout_sym.cpp9
-rw-r--r--test/CXX/symex/libc++/dynamic_cast.cpp7
-rw-r--r--test/CXX/symex/libc++/vector.cpp7
-rw-r--r--test/lit.cfg4
-rw-r--r--test/lit.site.cfg.in1
-rw-r--r--tools/klee/main.cpp9
9 files changed, 39 insertions, 26 deletions
diff --git a/test/CXX/symex/libc++/atexit.cpp b/test/CXX/symex/libc++/atexit.cpp
index 3d9e6834..79be6aa2 100644
--- a/test/CXX/symex/libc++/atexit.cpp
+++ b/test/CXX/symex/libc++/atexit.cpp
@@ -1,4 +1,7 @@
-// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include" | FileCheck %s
+// REQUIRES: libcxx
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc | FileCheck %s
 //
 // CHECK: Returning from main
 // CHECK: atexit_1
diff --git a/test/CXX/symex/libc++/compile_with_libcxx.sh b/test/CXX/symex/libc++/compile_with_libcxx.sh
deleted file mode 100644
index 8c45ec62..00000000
--- a/test/CXX/symex/libc++/compile_with_libcxx.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-set -x
-set -e
-set -o
-set -u
-
-COMPILER=$1
-FILENAME=$2
-CURDIR=$3
-TMPNAME=$4
-KLEE=$5
-INCLUDE_DIR=$6
-
-$COMPILER $FILENAME -std=c++11 -I ${INCLUDE_DIR} -emit-llvm -O0 -c -g -nostdinc++ -o ${TMPNAME}.bc
-rm -rf ${TMPNAME}.klee-out
-$KLEE --output-dir=${TMPNAME}.klee-out --no-output --exit-on-error --libc=uclibc --use-libcxx ${TMPNAME}.bc 2>&1
diff --git a/test/CXX/symex/libc++/cout.cpp b/test/CXX/symex/libc++/cout.cpp
index 2539b67f..e8b6e52f 100644
--- a/test/CXX/symex/libc++/cout.cpp
+++ b/test/CXX/symex/libc++/cout.cpp
@@ -1,4 +1,10 @@
-// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
+// REQUIRES: libcxx
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s
+
+// CHECK-DAG: cout
+// CHECK-DAG: cerr
 
 #include <iostream>
 
diff --git a/test/CXX/symex/libc++/cout_sym.cpp b/test/CXX/symex/libc++/cout_sym.cpp
index 52e59f05..6c6f2789 100644
--- a/test/CXX/symex/libc++/cout_sym.cpp
+++ b/test/CXX/symex/libc++/cout_sym.cpp
@@ -1,4 +1,11 @@
-// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
+// REQUIRES: libcxx
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc | FileCheck %s
+
+// CHECK-DAG: greater
+// CHECK-DAG: lower
+
 
 #include <iostream>
 #include "klee/klee.h"
diff --git a/test/CXX/symex/libc++/dynamic_cast.cpp b/test/CXX/symex/libc++/dynamic_cast.cpp
index 53e5bc69..e35e04d7 100644
--- a/test/CXX/symex/libc++/dynamic_cast.cpp
+++ b/test/CXX/symex/libc++/dynamic_cast.cpp
@@ -1,5 +1,8 @@
-// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
-
+// REQUIRES: libcxx
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc
+//
 // Copied from 'http://en.cppreference.com/w/cpp/language/dynamic_cast'
 
 struct V {
diff --git a/test/CXX/symex/libc++/vector.cpp b/test/CXX/symex/libc++/vector.cpp
index 27f5daba..1be87f80 100644
--- a/test/CXX/symex/libc++/vector.cpp
+++ b/test/CXX/symex/libc++/vector.cpp
@@ -1,5 +1,8 @@
-// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include" | FileCheck %s
-
+// REQUIRES: libcxx
+// RUN: %clangxx %s -emit-llvm %O0opt -c -std=c++11 -I "%libcxx_include" -g -nostdinc++ -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --libcxx %t1.bc 2>&1 | FileCheck %s
+//
 // CHECK: KLEE: done: completed paths = 1
 
 #include "klee/klee.h"
diff --git a/test/lit.cfg b/test/lit.cfg
index 1dafa911..05dfd7f1 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -189,6 +189,10 @@ config.available_features.add('zlib' if config.enable_zlib else 'not-zlib')
 if config.enable_posix_runtime:
   config.available_features.add('posix-runtime')
 
+# LibC++ runtime feature
+if config.enable_libcxx:
+  config.available_features.add('{}libcxx'.format('' if config.enable_libcxx else 'not-'))
+
 # Target operating system features
 supported_targets = ['linux', 'darwin']
 for target in supported_targets:
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index e0827559..6ee041d1 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -31,6 +31,7 @@ if @LLVM_VERSION_MAJOR@ >= 5:
 # Features
 config.enable_uclibc = True if @ENABLE_UCLIBC@ == 1 else False
 config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False
+config.enable_libcxx = True if @SUPPORT_KLEE_LIBCXX@ == 1 else False
 config.have_selinux = True if @HAVE_SELINUX@ == 1 else False
 config.enable_stp = True if @ENABLE_STP@ == 1 else False
 config.enable_z3 = True if @ENABLE_Z3@ == 1 else False
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 4e04dacc..ee115de3 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -289,9 +289,10 @@ namespace {
            cl::cat(TerminationCat));
 
   cl::opt<bool>
-  UseLibcxx("use-libcxx",
-           cl::desc("Link the llvm libc++ library into the bitcode"),
-           cl::init(0));
+  Libcxx("libcxx",
+           cl::desc("Link the llvm libc++ library into the bitcode (default=false)"),
+           cl::init(false),
+           cl::cat(LinkCat));
 }
 
 namespace klee {
@@ -1267,7 +1268,7 @@ int main(int argc, char **argv, char **envp) {
     preparePOSIX(loadedModules, libcPrefix);
   }
 
-  if (UseLibcxx) {
+  if (Libcxx) {
 #ifndef SUPPORT_KLEE_LIBCXX
     klee_error("Klee was not compiled with libcxx support");
 #else