From 9481fd85532187ebcdff0e9d7ab8efaaa05a4149 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 5 Jun 2017 10:38:17 +0100 Subject: Fix test failure on systems with libstdc++ corresponding to gcc7. This fixes #664. As reported by @jirislaby the `test/Feature/LongDouble.cpp` test fails to compile with Clang 3.4 due to new changes the libstdc++ headers. This ends up giving errors like ``` In file included from /home/abuild/rpmbuild/BUILD/klee-1.3.0+20170409/test/Feature/LongDouble.cpp:12: In file included from /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/cstdlib:77: /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:101:3: error: unknown type name '__float128' __float128 ^ /usr/bin/../lib64/gcc/x86_64-suse-linux/7/../../../../include/c++/7/bits/std_abs.h:102:7: error: unknown type name '__float128' abs(__float128 __x) ^ 2 errors generated. ``` Clang 4.0 seems fine with this source file so the problem has already been addressed upstream so we don't need to file a bug. We just need to move to a newer LLVM version to fix this properly! To work around this the test has been made into a C program rather than a C++ program to avoid including the C++ headers. The program wasn't using any important C++ features anyway so this seems like a sensible change. --- test/Feature/LongDouble.c | 61 ++++++++++++++++++++++++++++++++++++++++++ test/Feature/LongDouble.cpp | 64 --------------------------------------------- 2 files changed, 61 insertions(+), 64 deletions(-) create mode 100644 test/Feature/LongDouble.c delete mode 100644 test/Feature/LongDouble.cpp diff --git a/test/Feature/LongDouble.c b/test/Feature/LongDouble.c new file mode 100644 index 00000000..ad4c1a79 --- /dev/null +++ b/test/Feature/LongDouble.c @@ -0,0 +1,61 @@ +// RUN: %llvmgcc -g -emit-llvm -O0 -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log +// FIXME: When we remove LLVM 2.9 support just use FileCheck and remove these `grep`s. +// RUN: grep -q powl\(-11\\.0,0\)=1\\.0\\+ %t.log +// RUN: grep -q powl\(-11\\.0,1\)=-11\\.0\\+ %t.log +// RUN: grep -q powl\(-11\\.0,2\)=121\\.0\\+ %t.log +// RUN: grep -q 1/0=inf %t.log +// RUN: grep -q 1/-1=-1\\.0\\+ %t.log +// RUN: grep -q 1/-2=-0\\.50\\+ %t.log + +#include "klee/klee.h" +#include +#include +#include +#include + +unsigned klee_urange(unsigned start, unsigned end) { + unsigned x; + klee_make_symbolic(&x, sizeof x, "x"); + if (x - start >= end - start) + klee_silent_exit(0); + return x; +} + +int main(int argc, char **argv) { + int a = klee_urange(0, 3); + int b; + + // fork states + switch (a) { + case 0: + b = -0; + break; + case 1: + b = -1; + break; + case 2: + b = -2; + break; + default: + assert(0 && "Impossible switch target"); + } + + // test 80-bit external dispatch + long double d = powl((long double)-11.0, (long double)a); + // FIXME: Use CHECK-DAG: with FileCheck tool + // CHECK-DAG: powl(-11.0,0)=1.0 + // CHECK-DAG: powl(-11.0,1)=-11.0 + // CHECK-DAG: powl(-11.0,2)=121.0 + printf("powl(-11.0,%d)=%Lf\n", a, d); + + // test 80-bit fdiv + long double e = (long double)1 / (long double)b; + // CHECK-DAG: 1/0=inf + // CHECK-DAG: 1/1-1=-1.0 + // CHECK-DAG: 1/-2=-0.50 + printf("1/%d=%Lf\n", b, e); + + return 0; +} diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.cpp deleted file mode 100644 index 08924293..00000000 --- a/test/Feature/LongDouble.cpp +++ /dev/null @@ -1,64 +0,0 @@ -// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s -// RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log -// RUN: grep -q powl\(-11\\.0,0\)=1\\.0\\+ %t.log -// RUN: grep -q powl\(-11\\.0,1\)=-11\\.0\\+ %t.log -// RUN: grep -q powl\(-11\\.0,2\)=121\\.0\\+ %t.log -// RUN: grep -q 1/0=inf %t.log -// RUN: grep -q 1/-1=-1\\.0\\+ %t.log -// RUN: grep -q 1/-2=-0\\.50\\+ %t.log - -#include -#include -#include -#include - -#include "klee/klee.h" - -unsigned klee_urange(unsigned start, unsigned end) { - unsigned x; - klee_make_symbolic(&x, sizeof x, "x"); - if (x-start>=end-start) klee_silent_exit(0); - return x; -} - -int main(int argc, char ** argv) -{ - - int a = klee_urange(0,3); - int b; - - // fork states - switch(a) { - case 0: - b = -0; - break; - case 1: - b = -1; - break; - case 2: - b = -2; - break; - default: - assert(false && "Impossible switch target"); - } - - // test 80-bit external dispatch - long double d = powl((long double)-11.0, (long double)a); - // FIXME: Use CHECK-DAG: with FileCheck tool - // CHECK-DAG: powl(-11.0,0)=1.0 - // CHECK-DAG: powl(-11.0,1)=-11.0 - // CHECK-DAG: powl(-11.0,2)=121.0 - printf("powl(-11.0,%d)=%Lf\n", a, d); - - // test 80-bit fdiv - long double e = (long double) 1 / (long double) b; - // CHECK-DAG: 1/0=inf - // CHECK-DAG: 1/1-1=-1.0 - // CHECK-DAG: 1/-2=-0.50 - printf("1/%d=%Lf\n", b, e); - - return 0; -} - - -- cgit 1.4.1