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
