[klee-dev] Inquiry on path record and reply component of KLEE

[Cristian Cadar]

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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>