diff options
| -rw-r--r-- | test/Feature/LongDouble.c (renamed from test/Feature/LongDouble.cpp) | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.c index 08924293..ad4c1a79 100644 --- a/test/Feature/LongDouble.cpp +++ b/test/Feature/LongDouble.c @@ -1,6 +1,7 @@ -// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s +// 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 @@ -8,28 +9,26 @@ // RUN: grep -q 1/-1=-1\\.0\\+ %t.log // RUN: grep -q 1/-2=-0\\.50\\+ %t.log -#include <cstdio> -#include <cstdlib> -#include <cmath> -#include <cassert> - #include "klee/klee.h" +#include <assert.h> +#include <math.h> +#include <stdio.h> +#include <stdlib.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); + if (x - start >= end - start) + klee_silent_exit(0); return x; } -int main(int argc, char ** argv) -{ - - int a = klee_urange(0,3); +int main(int argc, char **argv) { + int a = klee_urange(0, 3); int b; // fork states - switch(a) { + switch (a) { case 0: b = -0; break; @@ -40,7 +39,7 @@ int main(int argc, char ** argv) b = -2; break; default: - assert(false && "Impossible switch target"); + assert(0 && "Impossible switch target"); } // test 80-bit external dispatch @@ -52,7 +51,7 @@ int main(int argc, char ** argv) printf("powl(-11.0,%d)=%Lf\n", a, d); // test 80-bit fdiv - long double e = (long double) 1 / (long double) b; + 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 @@ -60,5 +59,3 @@ int main(int argc, char ** argv) return 0; } - - |