From 8bec949fc84d8fe8dacbf38ff123b404f1eb4737 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Wed, 13 Dec 2017 17:37:16 +0000 Subject: Add support for concretizing symbolic objects passed to external functions --- test/Runtime/POSIX/MixedConcreteSymbolic.c | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 test/Runtime/POSIX/MixedConcreteSymbolic.c (limited to 'test/Runtime/POSIX/MixedConcreteSymbolic.c') diff --git a/test/Runtime/POSIX/MixedConcreteSymbolic.c b/test/Runtime/POSIX/MixedConcreteSymbolic.c new file mode 100644 index 00000000..48e06934 --- /dev/null +++ b/test/Runtime/POSIX/MixedConcreteSymbolic.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -allow-external-sym-calls --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 2>%t.log | FileCheck %s + +#include "klee/klee.h" +#include +#include + +int main(int argc, char **argv) { + char buf[32]; + + fread(buf, 1, 4, stdin); + klee_assume(buf[0] == 'a'); + klee_assume(buf[1] > 'a'); + klee_assume(buf[1] < 'z'); + klee_assume(buf[2] == '\n'); + klee_assume(buf[3] == '\0'); + fwrite(buf, 1, 4, stdout); + //CHECK: a{{[b-y]}} + + return 0; +} -- cgit 1.4.1