Hi,
On 21/09/2021 09:00, zy j wrote:
Hi,
I want to collect the path constraints of a specific PoC generated by
fuzzing, I have found similar question in
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html
<https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html>,
which helps a lot, I added --use-query-log=all:smt2,solver:smt2
--write-cvcs --write-smt2s to dump the constraints into files, and I got
the test000001.cvc and test000001.smt2 successfully.
Considering my purpose is to get the path constraints of given PoC, I
should use test000001.smt2 file, right? But the constraints in that file
are very few, seems they are not in accumulate mode, but only record the
constraints for the last branch. If I want to collect the whole path
constraints for a given PoC (if there are 20 branches before crash, I
want to collect all of the 20 branches' constraints), how can I do that?
I'm not sure what is the exact question here, but test*.smt2 should
contain the path condition associated with that path.
Besides, I also noticed that there was a command line option named
--write-pcs, which seems to be what I need:
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00636.html
<https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00636.html>.
However, there is no --write-pcs in the latest version, is it replaced
by other option?
It is now --write-kqueries
Best,
Cristian
Best regards,
Jiang
_______________________________________________
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
