[klee-dev] How to interpret a .path file?

[sudiptac]

Hi,
     I believe that the file with ".path" can be used for using the KLEE 
replay feature.

     In particular, "0" and "1" in each line, captures the outcome of 
branches ("false" leg and "true" leg)
for a particular execution. Note that each line is one instance for a 
branch instruction, during the execution.
Therefore, even though, a test program have very few static branch 
instructions, number of "0" and "1"
can be much higher during the execution time (depending on the number of 
times a branch is executed).

     Once a .path file is generated, KLEE can be given that file (using 
-replay-path feature) to execute the
specific path, instead of forking at the site of symbolic branches.

     Hope this helps.

Regards,
Sudipta


On 04/07/2015 08:11 AM, Zehra Naz wrote:
> Hi Klee-dev,
>
> This question has been asked before, but no concrete answer. The file 
> is a made up of about 395 0s and 1s, each on a separate line. This is 
> generated for get_sign.o which is a very short example and doesn't 
> have that many paths. What do the 1s and 0s mean?
>
>
> Thank you!
>
> Zehra
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed