Hi Harper,
As I mentioned on GitHub, the .path feature is currently unmaintained,
but it would be great to revive it.
Best,
Cristian
On 10/07/2021 15:24, Wei Chen wrote:
Dear developers,
Hi, I found there is a case that KLEE would generate the same .path
files for different paths in programs. Further, when given different
path files, the replay feature of Klee produces the same input for these
two paths. Here are the details:
For the attached file test_1.c, the aforementioned problem can be
reproduced by executing the following commands:
Attachment-1.png
KLEE would generate 3 paths for this program, then unfortunately
klee-out-0/test000002.path and klee-out-0/test000003.path are exactly
the same as each other. That’s weird because they are regarded as
different paths by klee.
For the replay feature of klee, given klee-out-0/test000001.path and
klee-out-0/test000002.path (two different paths), by executing klee with
—-replay-path option, two paths will be replayed and two test cases will
be generated.
However, the two test cases klee-out-1/test000001.ktest and
klee-out-2/test000001.ktest are exactly the same with each other.
Attachment.png
The attachment test_2.c also has the same .path problem, but the reply
feature works fine.
In that case, I’m wondering if there are some bugs inside the
path-related component of klee. The version of klee that I used is shown
as below:
image.png
Looking forward to your kind reply.
Best,
Harper
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
