diff options
author | Daniel Dunbar <daniel@zuster.org> | 2010-04-05 06:48:10 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2010-04-05 06:48:10 +0000 |
commit | 54d4d6353076800e0b640a380ce41e64f1041fbe (patch) | |
tree | ee8017b21860ce0fc9ee11520c16b3067e88496c /test | |
parent | cae0864b2437111b6cbbb7a3030e82bcef1a6024 (diff) | |
download | klee-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.cpp | 56 |
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; +} + + |