aboutsummaryrefslogtreecommitdiffhomepage
path: root/test/Feature
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature')
-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;
}
-
-