Hi,
I am trying to replay the KLEE testcases on my simple example. But I get an
error message:
** ERROR: out of inputs, using zero
More in details, my example is marking the symbolic inputs in a FOR loop, I
am
wondering if this is the source of the problem.
---
int main (int argc, char** argv) {
int dir;
int i;
for (i = 0; i < 10; i ++)
{
klee_make_symbolic(&dir, sizeof(int), "dir");
klee_assume (-1 <= dir);
klee_assume (dir <= 1);
process(dir);
}
return 0;
}
---
I hereby attach a self-contained package, if you like to try:
$ ./kcompile test02_klee.c
$ ./krun test02_klee.bc
$ ./kreplay test02_klee.c
The same example, i.e. test02_klee.c, can be compiled and run normally:
$ gcc test02_klee.c -DVERBOSE -o test02_klee
$ ./test02_klee
# 0 --[1] --> 1
# 1 --[-1] --> 1
# 1 --[1] --> 2
# 2 --[0] --> 2
# 2 --[1] --> 3
# 3 --[0] --> 3
# 3 --[-1] --> 2
# 2 --[-1] --> 1
# 1 --[-1] --> 1
# 1 --[0] --> 1
Thanks,
G.
