[klee-dev] Test cases generated for symbolic file

[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., 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>