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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
