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.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
