about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
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
+}