about summary refs log tree commit diff homepage
path: root/test/Feature
diff options
context:
space:
mode:
authorRichard Trembecký <richardt@centrum.sk>2016-04-29 22:33:41 +0200
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-05-24 14:08:27 +0100
commita0cd85b41f02ce5c476612eec182aa1ff3e6fe2b (patch)
treeb7d938116cae4f4a18225e9aef2f8934b761e063 /test/Feature
parent870f2d6aac35457e7524078a4b4a8b011f84c45c (diff)
downloadklee-a0cd85b41f02ce5c476612eec182aa1ff3e6fe2b.tar.gz
test: add versions of some tests for LLVM 3.7
Clone some tests to have their 3.7 version. 'call's, 'load's and
'getelementptr's match the new specification in them.

@andreamattavelli: Fixed test cases: BitCastAlias test cases included
modification to alias specifications that require LLVM 3.8

[v2] added comments what was changed and why
[v3] the new tests are without suffix, the old ones have ".leq36".

Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
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