aboutsummaryrefslogtreecommitdiffhomepage
path: root/test/Feature
diff options
context:
space:
mode:
Diffstat (limited to 'test/Feature')
-rw-r--r--test/Feature/BitcastAlias.leq36.ll35
-rw-r--r--test/Feature/BitcastAlias.ll9
-rw-r--r--test/Feature/BitcastAliasMD2U.leq36.ll35
-rw-r--r--test/Feature/BitcastAliasMD2U.ll9
-rw-r--r--test/Feature/ConstantArray.leq36.ll52
-rw-r--r--test/Feature/ConstantArray.ll32
-rw-r--r--test/Feature/ConstantStruct.leq36.ll34
-rw-r--r--test/Feature/ConstantStruct.ll6
-rw-r--r--test/Feature/GetElementPtr.leq36.ll30
-rw-r--r--test/Feature/GetElementPtr.ll10
-rw-r--r--test/Feature/InsertExtractValue.leq36.ll34
-rw-r--r--test/Feature/InsertExtractValue.ll6
-rw-r--r--test/Feature/Overflow.leq36.ll45
-rw-r--r--test/Feature/Overflow.ll6
-rw-r--r--test/Feature/OverflowMul.leq36.ll45
-rw-r--r--test/Feature/OverflowMul.ll6
-rw-r--r--test/Feature/_utils._ll39
-rw-r--r--test/Feature/_utils.leq36._ll71
18 files changed, 454 insertions, 50 deletions
diff --git a/test/Feature/BitcastAlias.leq36.ll b/test/Feature/BitcastAlias.leq36.ll
new file mode 100644
index 00000000..d203e52c
--- /dev/null
+++ b/test/Feature/BitcastAlias.leq36.ll
@@ -0,0 +1,35 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+@foo = alias i32 (i32)* @__foo
+
+define i32 @__foo(i32 %i) nounwind {
+entry:
+ ret i32 %i
+}
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+ %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+ %r = icmp eq i32 %call, 52
+ br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/BitcastAlias.ll b/test/Feature/BitcastAlias.ll
index e0e3653f..5bd30193 100644
--- a/test/Feature/BitcastAlias.ll
+++ b/test/Feature/BitcastAlias.ll
@@ -1,3 +1,6 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -20,15 +23,15 @@ declare i32 @puts(i8*)
define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
entry:
- %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+ %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
%r = icmp eq i32 %call, 52
br i1 %r, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/BitcastAliasMD2U.leq36.ll b/test/Feature/BitcastAliasMD2U.leq36.ll
new file mode 100644
index 00000000..cef8ac54
--- /dev/null
+++ b/test/Feature/BitcastAliasMD2U.leq36.ll
@@ -0,0 +1,35 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+@foo = alias i32 (i32)* @__foo
+
+define i32 @__foo(i32 %i) nounwind {
+entry:
+ ret i32 %i
+}
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+ %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+ %r = icmp eq i32 %call, 52
+ br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/BitcastAliasMD2U.ll b/test/Feature/BitcastAliasMD2U.ll
index 24eabaa5..7eddd3d6 100644
--- a/test/Feature/BitcastAliasMD2U.ll
+++ b/test/Feature/BitcastAliasMD2U.ll
@@ -1,3 +1,6 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2
@@ -20,15 +23,15 @@ declare i32 @puts(i8*)
define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
entry:
- %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
+ %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52)
%r = icmp eq i32 %call, 52
br i1 %r, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/ConstantArray.leq36.ll b/test/Feature/ConstantArray.leq36.ll
new file mode 100644
index 00000000..a4986ff4
--- /dev/null
+++ b/test/Feature/ConstantArray.leq36.ll
@@ -0,0 +1,52 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc 2>&1 | FileCheck %s
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"0\00", align 1
+@.str2 = private unnamed_addr constant [2 x i8] c"1\00", align 1
+
+%struct.dirent = type { i32, i32, i16, i8 }
+declare void @klee_print_expr(i8*, ...)
+
+define i32 @main() {
+entry:
+ %a = alloca %struct.dirent
+ %tmp1 = getelementptr %struct.dirent* %a, i32 0
+ %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>*
+ ; Initialize with constant vector
+ store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2
+ br label %exit
+exit:
+ ; Print first initialized element
+ %idx = getelementptr %struct.dirent* %a, i32 0, i32 0
+ %val = load i32* %idx
+ call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val)
+ ; CHECK: 0:42
+
+ ; Print second initialized element
+ %idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1
+ %val2 = load i32* %idx2
+ call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val2)
+ ; CHECK: 1:4096
+
+ ; Initialize with constant array
+ %array = alloca [2 x i32];
+ store [2 x i32][i32 7, i32 9], [2 x i32]* %array
+
+ ; Print first initialized element
+ %idx3 = getelementptr [2 x i32]* %array, i32 0, i32 0
+ %val3 = load i32* %idx3
+ call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val3)
+ ; CHECK: 0:7
+
+ ; Print second initialized element
+ %idx4 = getelementptr [2 x i32]* %array, i32 0, i32 1
+ %val4 = load i32* %idx4
+ call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val4)
+ ; CHECK: 1:9
+
+ ret i32 0
+}
diff --git a/test/Feature/ConstantArray.ll b/test/Feature/ConstantArray.ll
index 161b2a16..195b4cb0 100644
--- a/test/Feature/ConstantArray.ll
+++ b/test/Feature/ConstantArray.ll
@@ -1,3 +1,7 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+; LLVM 3.7 no longer accepts '*' with a 'call'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc 2>&1 | FileCheck %s
@@ -13,22 +17,22 @@ declare void @klee_print_expr(i8*, ...)
define i32 @main() {
entry:
%a = alloca %struct.dirent
- %tmp1 = getelementptr %struct.dirent* %a, i32 0
+ %tmp1 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0
%tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>*
; Initialize with constant vector
store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2
br label %exit
exit:
; Print first initialized element
- %idx = getelementptr %struct.dirent* %a, i32 0, i32 0
- %val = load i32* %idx
- call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val)
+ %idx = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 0
+ %val = load i32, i32* %idx
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val)
; CHECK: 0:42
; Print second initialized element
- %idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1
- %val2 = load i32* %idx2
- call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val2)
+ %idx2 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 1
+ %val2 = load i32, i32* %idx2
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val2)
; CHECK: 1:4096
; Initialize with constant array
@@ -36,16 +40,16 @@ exit:
store [2 x i32][i32 7, i32 9], [2 x i32]* %array
; Print first initialized element
- %idx3 = getelementptr [2 x i32]* %array, i32 0, i32 0
- %val3 = load i32* %idx3
- call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val3)
+ %idx3 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 0
+ %val3 = load i32, i32* %idx3
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val3)
; CHECK: 0:7
; Print second initialized element
- %idx4 = getelementptr [2 x i32]* %array, i32 0, i32 1
- %val4 = load i32* %idx4
- call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val4)
+ %idx4 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 1
+ %val4 = load i32, i32* %idx4
+ call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val4)
; CHECK: 1:9
ret i32 0
-} \ No newline at end of file
+}
diff --git a/test/Feature/ConstantStruct.leq36.ll b/test/Feature/ConstantStruct.leq36.ll
new file mode 100644
index 00000000..073544d3
--- /dev/null
+++ b/test/Feature/ConstantStruct.leq36.ll
@@ -0,0 +1,34 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+%struct.sfoo = type { i32, i64 }
+
+declare i32 @puts(i8*)
+declare i32 @printf(i8*, ...)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+ %f0 = extractvalue %struct.sfoo { i32 3, i64 1 }, 0
+ %f1 = extractvalue %struct.sfoo { i32 3, i64 1 }, 1
+ %xf0 = zext i32 %f0 to i64
+ %f0mf1 = sub i64 %xf0, %f1
+ %r = icmp eq i64 %f0mf1, 2
+ br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/ConstantStruct.ll b/test/Feature/ConstantStruct.ll
index 4fe6b5d0..e4b3d07b 100644
--- a/test/Feature/ConstantStruct.ll
+++ b/test/Feature/ConstantStruct.ll
@@ -1,3 +1,5 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -24,10 +26,10 @@ entry:
br i1 %r, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/GetElementPtr.leq36.ll b/test/Feature/GetElementPtr.leq36.ll
new file mode 100644
index 00000000..43f33e27
--- /dev/null
+++ b/test/Feature/GetElementPtr.leq36.ll
@@ -0,0 +1,30 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main() {
+entry:
+ %addr = alloca i8, align 4
+ %addrp1 = getelementptr i8* %addr, i32 1
+ %addrp1m1 = getelementptr i8* %addrp1, i32 -1
+ %test = icmp eq i8* %addr, %addrp1m1
+ br i1 %test, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/GetElementPtr.ll b/test/Feature/GetElementPtr.ll
index da94441c..f7f8aada 100644
--- a/test/Feature/GetElementPtr.ll
+++ b/test/Feature/GetElementPtr.ll
@@ -1,3 +1,5 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -14,16 +16,16 @@ declare i32 @puts(i8*)
define i32 @main() {
entry:
%addr = alloca i8, align 4
- %addrp1 = getelementptr i8* %addr, i32 1
- %addrp1m1 = getelementptr i8* %addrp1, i32 -1
+ %addrp1 = getelementptr i8, i8* %addr, i32 1
+ %addrp1m1 = getelementptr i8, i8* %addrp1, i32 -1
%test = icmp eq i8* %addr, %addrp1m1
br i1 %test, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/InsertExtractValue.leq36.ll b/test/Feature/InsertExtractValue.leq36.ll
new file mode 100644
index 00000000..431e14c4
--- /dev/null
+++ b/test/Feature/InsertExtractValue.leq36.ll
@@ -0,0 +1,34 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+%struct.sfoo = type { i32, i32 }
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone {
+entry:
+ %s0 = insertvalue %struct.sfoo undef, i32 3, 0
+ %s1 = insertvalue %struct.sfoo %s0, i32 1, 1
+ %f0 = extractvalue %struct.sfoo %s1, 0
+ %f1 = extractvalue %struct.sfoo %s1, 1
+ %f0mf1 = sub i32 %f0, %f1
+ %r = icmp eq i32 %f0mf1, 2
+ br i1 %r, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/InsertExtractValue.ll b/test/Feature/InsertExtractValue.ll
index 83e8f851..fff6da7c 100644
--- a/test/Feature/InsertExtractValue.ll
+++ b/test/Feature/InsertExtractValue.ll
@@ -1,3 +1,5 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -24,10 +26,10 @@ entry:
br i1 %r, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/Overflow.leq36.ll b/test/Feature/Overflow.leq36.ll
new file mode 100644
index 00000000..2ab04772
--- /dev/null
+++ b/test/Feature/Overflow.leq36.ll
@@ -0,0 +1,45 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+declare {i8, i1} @llvm.uadd.with.overflow.i8(i8 %a, i8 %b)
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main() {
+bb0:
+ %s0 = call {i8, i1} @llvm.uadd.with.overflow.i8(i8 0, i8 -1)
+ %v0 = extractvalue {i8, i1} %s0, 0
+ %c0 = icmp eq i8 %v0, -1
+ br i1 %c0, label %bb0_1, label %bbfalse
+
+bb0_1:
+ %o0 = extractvalue {i8, i1} %s0, 1
+ br i1 %o0, label %bbfalse, label %bb1
+
+bb1:
+ %s1 = call {i8, i1} @llvm.uadd.with.overflow.i8(i8 1, i8 -1)
+ %v1 = extractvalue {i8, i1} %s1, 0
+ %c1 = icmp eq i8 %v1, 0
+ br i1 %c1, label %bb1_1, label %bbfalse
+
+bb1_1:
+ %o1 = extractvalue {i8, i1} %s1, 1
+ br i1 %o1, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/Overflow.ll b/test/Feature/Overflow.ll
index 35dfbd10..1dbe1216 100644
--- a/test/Feature/Overflow.ll
+++ b/test/Feature/Overflow.ll
@@ -1,3 +1,5 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -35,10 +37,10 @@ bb1_1:
br i1 %o1, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/OverflowMul.leq36.ll b/test/Feature/OverflowMul.leq36.ll
new file mode 100644
index 00000000..1b14d380
--- /dev/null
+++ b/test/Feature/OverflowMul.leq36.ll
@@ -0,0 +1,45 @@
+; REQUIRES: lt-llvm-3.7
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+declare {i8, i1} @llvm.umul.with.overflow.i8(i8 %a, i8 %b)
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main() {
+bb0:
+ %s0 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 1, i8 128)
+ %v0 = extractvalue {i8, i1} %s0, 0
+ %c0 = icmp eq i8 %v0, 128
+ br i1 %c0, label %bb0_1, label %bbfalse
+
+bb0_1:
+ %o0 = extractvalue {i8, i1} %s0, 1
+ br i1 %o0, label %bbfalse, label %bb1
+
+bb1:
+ %s1 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 2, i8 128)
+ %v1 = extractvalue {i8, i1} %s1, 0
+ %c1 = icmp eq i8 %v1, 0
+ br i1 %c1, label %bb1_1, label %bbfalse
+
+bb1_1:
+ %o1 = extractvalue {i8, i1} %s1, 1
+ br i1 %o1, label %bbtrue, label %bbfalse
+
+bbtrue:
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ ret i32 0
+
+bbfalse:
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ ret i32 0
+}
diff --git a/test/Feature/OverflowMul.ll b/test/Feature/OverflowMul.ll
index 7026aa74..3173e43c 100644
--- a/test/Feature/OverflowMul.ll
+++ b/test/Feature/OverflowMul.ll
@@ -1,3 +1,5 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; REQUIRES: geq-llvm-3.7
; RUN: llvm-as %s -f -o %t1.bc
; RUN: rm -rf %t.klee-out
; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2
@@ -35,10 +37,10 @@ bb1_1:
br i1 %o1, label %bbtrue, label %bbfalse
bbtrue:
- %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+ %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind
ret i32 0
bbfalse:
- %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+ %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind
ret i32 0
}
diff --git a/test/Feature/_utils._ll b/test/Feature/_utils._ll
index 32a73bb1..d825df3a 100644
--- a/test/Feature/_utils._ll
+++ b/test/Feature/_utils._ll
@@ -1,3 +1,6 @@
+; LLVM 3.7 requires a type as the first argument to 'getelementptr'
+; LLVM 3.7 requires a type as the first argument to 'load'
+
define i32 @util_make_and_i1(i32 %a, i32 %b) {
%a_i1 = icmp ne i32 %a, 0
%b_i1 = icmp ne i32 %b, 0
@@ -17,26 +20,26 @@ define i32 @util_make_or_i1(i32 %a, i32 %b) {
define i16 @util_make_concat2(i8 %a, i8 %b) {
%tmp = alloca i16
%tmp8 = bitcast i16* %tmp to i8*
- %p0 = getelementptr i8* %tmp8, i32 0
- %p1 = getelementptr i8* %tmp8, i32 1
+ %p0 = getelementptr i8, i8* %tmp8, i32 0
+ %p1 = getelementptr i8, i8* %tmp8, i32 1
store i8 %b, i8* %p0
store i8 %a, i8* %p1
- %concat = load i16* %tmp
+ %concat = load i16, i16* %tmp
ret i16 %concat
}
define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) {
%tmp = alloca i32
%tmp8 = bitcast i32* %tmp to i8*
- %p0 = getelementptr i8* %tmp8, i32 0
- %p1 = getelementptr i8* %tmp8, i32 1
- %p2 = getelementptr i8* %tmp8, i32 2
- %p3 = getelementptr i8* %tmp8, i32 3
+ %p0 = getelementptr i8, i8* %tmp8, i32 0
+ %p1 = getelementptr i8, i8* %tmp8, i32 1
+ %p2 = getelementptr i8, i8* %tmp8, i32 2
+ %p3 = getelementptr i8, i8* %tmp8, i32 3
store i8 %d, i8* %p0
store i8 %c, i8* %p1
store i8 %b, i8* %p2
store i8 %a, i8* %p3
- %concat = load i32* %tmp
+ %concat = load i32, i32* %tmp
ret i32 %concat
}
@@ -44,14 +47,14 @@ define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d,
i8 %e, i8 %f, i8 %g, i8 %h) {
%tmp = alloca i64
%tmp8 = bitcast i64* %tmp to i8*
- %p0 = getelementptr i8* %tmp8, i32 0
- %p1 = getelementptr i8* %tmp8, i32 1
- %p2 = getelementptr i8* %tmp8, i32 2
- %p3 = getelementptr i8* %tmp8, i32 3
- %p4 = getelementptr i8* %tmp8, i32 4
- %p5 = getelementptr i8* %tmp8, i32 5
- %p6 = getelementptr i8* %tmp8, i32 6
- %p7 = getelementptr i8* %tmp8, i32 7
+ %p0 = getelementptr i8, i8* %tmp8, i32 0
+ %p1 = getelementptr i8, i8* %tmp8, i32 1
+ %p2 = getelementptr i8, i8* %tmp8, i32 2
+ %p3 = getelementptr i8, i8* %tmp8, i32 3
+ %p4 = getelementptr i8, i8* %tmp8, i32 4
+ %p5 = getelementptr i8, i8* %tmp8, i32 5
+ %p6 = getelementptr i8, i8* %tmp8, i32 6
+ %p7 = getelementptr i8, i8* %tmp8, i32 7
store i8 %h, i8* %p0
store i8 %g, i8* %p1
store i8 %f, i8* %p2
@@ -60,7 +63,7 @@ define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d,
store i8 %c, i8* %p5
store i8 %b, i8* %p6
store i8 %a, i8* %p7
- %concat = load i64* %tmp
+ %concat = load i64, i64* %tmp
ret i64 %concat
}
@@ -68,4 +71,4 @@ define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) {
%cond_i1 = icmp ne i32 %cond, 0
%res = select i1 %cond_i1, i32 %t, i32 %f
ret i32 %res
-} \ No newline at end of file
+}
diff --git a/test/Feature/_utils.leq36._ll b/test/Feature/_utils.leq36._ll
new file mode 100644
index 00000000..32a73bb1
--- /dev/null
+++ b/test/Feature/_utils.leq36._ll
@@ -0,0 +1,71 @@
+define i32 @util_make_and_i1(i32 %a, i32 %b) {
+ %a_i1 = icmp ne i32 %a, 0
+ %b_i1 = icmp ne i32 %b, 0
+ %res_i1 = and i1 %a_i1, %b_i1
+ %res = zext i1 %res_i1 to i32
+ ret i32 %res
+}
+
+define i32 @util_make_or_i1(i32 %a, i32 %b) {
+ %a_i1 = icmp ne i32 %a, 0
+ %b_i1 = icmp ne i32 %b, 0
+ %res_i1 = or i1 %a_i1, %b_i1
+ %res = zext i1 %res_i1 to i32
+ ret i32 %res
+}
+
+define i16 @util_make_concat2(i8 %a, i8 %b) {
+ %tmp = alloca i16
+ %tmp8 = bitcast i16* %tmp to i8*
+ %p0 = getelementptr i8* %tmp8, i32 0
+ %p1 = getelementptr i8* %tmp8, i32 1
+ store i8 %b, i8* %p0
+ store i8 %a, i8* %p1
+ %concat = load i16* %tmp
+ ret i16 %concat
+}
+
+define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) {
+ %tmp = alloca i32
+ %tmp8 = bitcast i32* %tmp to i8*
+ %p0 = getelementptr i8* %tmp8, i32 0
+ %p1 = getelementptr i8* %tmp8, i32 1
+ %p2 = getelementptr i8* %tmp8, i32 2
+ %p3 = getelementptr i8* %tmp8, i32 3
+ store i8 %d, i8* %p0
+ store i8 %c, i8* %p1
+ store i8 %b, i8* %p2
+ store i8 %a, i8* %p3
+ %concat = load i32* %tmp
+ ret i32 %concat
+}
+
+define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d,
+ i8 %e, i8 %f, i8 %g, i8 %h) {
+ %tmp = alloca i64
+ %tmp8 = bitcast i64* %tmp to i8*
+ %p0 = getelementptr i8* %tmp8, i32 0
+ %p1 = getelementptr i8* %tmp8, i32 1
+ %p2 = getelementptr i8* %tmp8, i32 2
+ %p3 = getelementptr i8* %tmp8, i32 3
+ %p4 = getelementptr i8* %tmp8, i32 4
+ %p5 = getelementptr i8* %tmp8, i32 5
+ %p6 = getelementptr i8* %tmp8, i32 6
+ %p7 = getelementptr i8* %tmp8, i32 7
+ store i8 %h, i8* %p0
+ store i8 %g, i8* %p1
+ store i8 %f, i8* %p2
+ store i8 %e, i8* %p3
+ store i8 %d, i8* %p4
+ store i8 %c, i8* %p5
+ store i8 %b, i8* %p6
+ store i8 %a, i8* %p7
+ %concat = load i64* %tmp
+ ret i64 %concat
+}
+
+define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) {
+ %cond_i1 = icmp ne i32 %cond, 0
+ %res = select i1 %cond_i1, i32 %t, i32 %f
+ ret i32 %res
+} \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-23 10:07:06 +0000