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