diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/Intrinsics/IsConstant.ll | 39 |
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 +} |