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 files, I get the stat from theactual files whose contents are loaded into the symbolic files. For stdin and stdout,I get the stats using fstat64 of file descriptors 0 and 1, respectively. I think model_version is mandatory if one wants to use the produced file as a seed.
I had submitted PR 917https://github.com/klee/klee/pull/917 But probably this PR will not pass the CI tests since I had not added the tests.I will also close it now since you publicly announced your tool first. Best,Andrew On Saturday, 23 June 2018, 1:13:31 am GMT+8, Sang Phan <phanquocs...@gmail.com> wrote: 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: https://github.com/qsphan/klee-utils/blob/master/src/gen-ktest.cpp + stat is generated randomly, copied from to gen-random-bout + model version is always set to 1 It seems to work just fine right now. But as both stat and model-version appear in the path condition, is there any possible problem with this settings? Best, Sang On Fri, Jun 22, 2018 at 9:47 AM, Cristian Cadar <c.ca...@imperial.ac.uk> wrote: > 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., at > http://klee.github.io/tutorials/using-symbolic/) by submitting a PR at > https://github.com/klee/klee.github.io > > Best, > Cristian > > > On 21/06/18 21:55, Sang Phan wrote: >> >> Hello, >> >> I'm trying to understand the test cases generated when the input is >> symbolic file. >> For the password example under this link: >> https://klee.github.io/tutorials/using-symbolic/, a test case viewed >> by ktest-tool is the following: >> >> https://klee.github.io/tutorials/using-symbolic/ >> >> >> ktest file : 'test000004.ktest' >> args : ['password.bc', 'A', '-sym-files', '1', '10'] >> num objects: 3 >> object 0: name: b'A-data' >> object 0: size: 10 >> object 0: data: b'hel\x00\x00\x00\x00\x00\x00\x00' >> object 1: name: b'A-data-stat' >> object 1: size: 144 >> object 1: data: >> >> b'\x05\x08\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\xa4\x81\x00\x00\xe8\x03\x00\x00\xe8\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xea\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x0e,[\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' >> object 2: name: b'model_version' >> object 2: size: 4 >> object 2: data: b'\x01\x00\x00\x00' >> >> + I understand A-data is the content of the file, but what is >> A-data-stat and model-version? >> + From the gen-random-bout, it seems data-stat can be generated >> randomly, but how about model-version? >> >> Thanks, >> Sang >> >> _______________________________________________ >> 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 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