1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
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 <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);
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;
}
|
