[klee-dev] Test cases generated for symbolic file

[Sang Phan]

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