Klee on seed mode does not support symbolic size in its own harness #51
Description
When launched a second time on a program taking an array and its size as arguments, with an array-size-mapping constraint, Klee does not manage to really continue its exploration of the program on the basis of the seeds given from the first execution. It emits an error message, generates a few tests that seem to be meaningless (no mention of ASSERTION FAILURE) and exits. On the contrary, if it is executed with a larger timeout, it manages to better cover the code and finds more tests (meaning that it did not really finished its exploration when it decided to exit).
The error message in the second execution is the following:
KLEE: allocating symbolic size (capacity = 20, at _sc/Problem01_revu.c-DC-@7/klee/harness.c:13)
KLEE: ERROR: _sc/Problem01_revu.c-DC-@7/klee/harness.c:13: no support for symbolic size in seed mode
I attach the code. The configuration file is the following :
[project]
ignored-globals = ["a","b","c","d","e","f","u","v","w","x","y","z","a17","a7","a20","a8","a12","a16","a21"]
files = ["Problem01_revu.c"]
criterion = "DC"
entrypoint = "main_problem"
[pointer-handling]
max-ptr-array-length = 5
array-size-mapping = ["inputs:nb"]
[klee]
timeout = 30.000