[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 
> <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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev