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
|
; REQUIRES: geq-llvm-12.0
; 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 {
smax:
%0 = call i32 @llvm.smax.i32(i32 -10, i32 10)
%cmp = icmp ne i32 %0, 10
br i1 %cmp, label %abort.block, label %smin
smin:
%1 = call i32 @llvm.smin.i32(i32 -10, i32 10)
%cmp1 = icmp ne i32 %1, -10
br i1 %cmp1, label %abort.block, label %umax
umax:
%2 = call i32 @llvm.umax.i32(i32 10, i32 20)
%cmp2 = icmp ne i32 %2, 20
br i1 %cmp2, label %abort.block, label %umin
umin:
%3 = call i32 @llvm.umin.i32(i32 10, i32 5)
%cmp3 = icmp ne i32 %3, 5
br i1 %cmp3, label %abort.block, label %exit.block
exit.block:
ret i32 0
abort.block:
call void @abort()
unreachable
}
declare void @abort() noreturn nounwind
declare i32 @llvm.smax.i32(i32, i32)
declare i32 @llvm.smin.i32(i32, i32)
declare i32 @llvm.umax.i32(i32, i32)
declare i32 @llvm.umin.i32(i32, i32)
|