Re: [klee-dev] Collect path constraints with seed mode

[Cristian Cadar]

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 
, 
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 test01.cvc and test01.smt2 successfully.


Considering my purpose is to get the path constraints of given PoC, I 
should use test01.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 
. 
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

[klee-dev] Collect path constraints with seed mode

[zy j]

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 test01.cvc and test01.smt2 successfully.

Considering my purpose is to get the path constraints of given PoC, I
should use test01.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
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev