[klee-dev] Bounded properties of linked lists

[Mario Alvarez Picallo]

Hello all,

I'm using Klee to verify properties of linked data structures, and I've run
into a small limitation while trying to verify this program[0].

My problem is that, intuitively, I see no reason for Klee to generate lists
of length > 1 in order to prove the specified property, since it doesn't
depend on anything but the head element, but Klee will still generate all
lists of any length and try all of them.

Is there any way to avoid this infinite search by using any of the options
already implemented in Klee? And, if not, how difficult would it be to add
such an option?

Thanks in advance,
Mario

[0] https://gist.github.com/m-alvarez/c082ffc28c523fc0a9d2

-- 
Now I do not know whether I was then a lambda expression emulating a Turing
machine, or whether I am a Turing machine emulating a lambda expression.
-------------- next part --------------
HTML attachment scrubbed and removed