Re: [klee-dev] Test cases generated for symbolic file

2018-06-23 Thread Andrew Santosa
Thanks Sang. I hope to find time to write the tests to make codecov happy. Andrew On Saturday, 23 June 2018, 2:33:20 pm GMT+8, Sang Phan wrote: Hi Andrew, I only build the tool for my own task, and I don't intend to submit a PR, so please go ahead with yours. Sang On Fri, Jun 22,

Re: [klee-dev] Test cases generated for symbolic file

2018-06-23 Thread Sang Phan
Hi Andrew, I only build the tool for my own task, and I don't intend to submit a PR, so please go ahead with yours. Sang On Fri, Jun 22, 2018 at 9:32 PM, Andrew Santosa wrote: > Hi Sang, > > I urgently need a tool like you mentioned, so I wrote one myself within KLEE > source tree. You can

Re: [klee-dev] Test cases generated for symbolic file

2018-06-22 Thread Andrew Santosa
Hi Sang, I urgently need a tool like you mentioned, so I wrote one myself within KLEEsource tree. You can find the source as tools/gen-bout.cpp in the gen-bout branchof my KLEE fork: https://github.com/domainexpert/klee/tree/gen-bout I don't exactly know the answer to your question. For normal

Re: [klee-dev] Test cases generated for symbolic file

2018-06-22 Thread Sang Phan
Thanks Cristian. I want to feed KLEE with my customized seeds, instead of random ones. So I need a tool similar to gen-random-bout to generate .ktest file. To write such a tool, I would like to know how to generate the stat and model-version Here is my quick implementation:

Re: [klee-dev] Test cases generated for symbolic file

2018-06-22 Thread Cristian Cadar
Hi, you can ignore the model_version, it just keeps track of the version for the POSIX model. The stat buffer keeps the stat info associated with the file (see e.g. http://man7.org/linux/man-pages/man2/stat.2.html). If you have time, it would be useful to document this on the website (e.g.,