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