[klee-dev] Collect path constraints with seed mode

zy j supermolejzy at gmail.com
Tue Sep 21 09:00:21 BST 2021


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, 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?

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.
However, there is no --write-pcs in the latest version, is it replaced by
other option?

Best regards,

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


More information about the klee-dev mailing list