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
|
; RUN: rm -rf %t.klee-out
; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %s
define dso_local i32 @main() local_unnamed_addr {
fma.float:
%0 = call float @llvm.fma.f32(float 2.0, float 2.0, float 1.0)
%cmp0 = fcmp one float %0, 5.0
br i1 %cmp0, label %abort.block, label %fma.double
fma.double:
%1 = call double @llvm.fma.f64(double 2.0, double 2.0, double 1.0)
%cmp1 = fcmp one double %1, 5.0
br i1 %cmp1, label %abort.block, label %fma.fp80
fma.fp80:
%2 = call x86_fp80 @llvm.fma.f80(x86_fp80 0xK40008000000000000000,
x86_fp80 0xK40008000000000000000,
x86_fp80 0xK3FFF8000000000000000)
%cmp2 = fcmp one x86_fp80 %2, 0xK4001A000000000000000
br i1 %cmp2, label %abort.block, label %fmuladd.float
fmuladd.float:
%3 = call float @llvm.fmuladd.f32(float 2.0, float 2.0, float 1.0)
%cmp3 = fcmp one float %3, 5.0
br i1 %cmp3, label %abort.block, label %fmuladd.double
fmuladd.double:
%4 = call double @llvm.fmuladd.f64(double 2.0, double 2.0, double 1.0)
%cmp4 = fcmp one double %4, 5.0
br i1 %cmp4, label %abort.block, label %fmuladd.fp80
fmuladd.fp80:
%5 = call x86_fp80 @llvm.fmuladd.f80(x86_fp80 0xK40008000000000000000,
x86_fp80 0xK40008000000000000000,
x86_fp80 0xK3FFF8000000000000000)
%cmp5 = fcmp one x86_fp80 %5, 0xK4001A000000000000000
br i1 %cmp4, label %abort.block, label %exit.block
exit.block:
ret i32 0
abort.block:
call void @abort()
unreachable
}
declare void @abort() noreturn nounwind
declare float @llvm.fma.f32(float %a, float %b, float %c)
declare double @llvm.fma.f64(double %a, double %b, double %c)
declare x86_fp80 @llvm.fma.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c)
declare float @llvm.fmuladd.f32(float %a, float %b, float %c)
declare double @llvm.fmuladd.f64(double %a, double %b, double %c)
declare x86_fp80 @llvm.fmuladd.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c)
|