about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2010-04-05 06:48:10 +0000
committerDaniel Dunbar <daniel@zuster.org>2010-04-05 06:48:10 +0000
commit54d4d6353076800e0b640a380ce41e64f1041fbe (patch)
treeee8017b21860ce0fc9ee11520c16b3067e88496c /test
parentcae0864b2437111b6cbbb7a3030e82bcef1a6024 (diff)
downloadklee-54d4d6353076800e0b640a380ce41e64f1041fbe.tar.gz
Add long double support, patch by David Ramos.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'test')
-rw-r--r--test/Feature/LongDouble.cpp56
1 files changed, 56 insertions, 0 deletions
diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.cpp
new file mode 100644
index 00000000..ecee43b4
--- /dev/null
+++ b/test/Feature/LongDouble.cpp
@@ -0,0 +1,56 @@
+// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s
+// RUN: %klee --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 <cstdio>
+#include <cstdlib>
+#include <cmath>
+#include <cassert>
+
+#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);
+  printf("powl(-11.0,%d)=%Lf\n", a, d);
+
+  // test 80-bit fdiv
+  long double e = (long double) 1 / (long double) b;
+  printf("1/%d=%Lf\n", b, e);
+
+  return 0;
+}
+
+