about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorGleb Popov <6yearold@gmail.com>2019-11-12 14:38:19 +0400
committerMartinNowack <martin.nowack@gmail.com>2019-11-15 15:43:11 +0000
commit3af34e6095ee64332c089c98128dcfbcccced65e (patch)
tree71f003c83f17a4c7bbd45f8b9436167dad8e7419 /test
parentc33beaa330bc8917249575b285f4a083dfe81922 (diff)
downloadklee-3af34e6095ee64332c089c98128dcfbcccced65e.tar.gz
Implement @llvm.is.constant() intrinsic handling and add a test for it.
Diffstat (limited to 'test')
-rw-r--r--test/Intrinsics/IsConstant.ll39
1 files changed, 39 insertions, 0 deletions
diff --git a/test/Intrinsics/IsConstant.ll b/test/Intrinsics/IsConstant.ll
new file mode 100644
index 00000000..b196d933
--- /dev/null
+++ b/test/Intrinsics/IsConstant.ll
@@ -0,0 +1,39 @@
+; REQUIRES: geq-llvm-8.0
+; RUN: %llvmas %s -o=%t.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %t.bc
+
+declare i1 @llvm.is.constant.i32(i32)
+
+declare i32 @klee_is_symbolic(i32)
+declare void @klee_abort(i8*)
+
+define i1 @check1() {
+  %r = call i1 @llvm.is.constant.i32(i32 123)
+
+  ret i1 %r
+}
+
+define i1 @check2() {
+  %x = call i32 @klee_is_symbolic(i32 0)
+
+  %r = call i1 @llvm.is.constant.i32(i32 %x)
+
+  %notR = xor i1 %r, 1
+
+  ret i1 %notR
+}
+
+define i32 @main() {
+  %r1 = call i1 @check1()
+  %r2 = call i1 @check2()
+
+  br i1 %r1, label %next, label %exitFalse
+next:
+  br i1 %r2, label %exitTrue, label %exitFalse
+exitFalse:
+  call void @klee_abort(i8* null)
+  ret i32 1
+exitTrue:
+  ret i32 0
+}