Hi All, I am trying to run KLEE on gzip to generate input test cases for the decompression. The problem i am facing is that all the test cases KLEE is generating are same and they all are all zeros. Can someone point out what i maybe doing wrong?
This is the command I am using : klee --only-output-states-covering-new \ --simplify-sym-indices \ --max-memory=1000 \ --disable-inlining \ --use-forked-stp -allow-external-sym-calls \ --max-instruction-time=30. \ --use-batching-search \ --batch-instructions=10000 \ --max-static-solve-pct=1 \ --max-static-cpfork-pct=1 \ --switch-type=internal \ --max-memory-inhibit=false \ --max-static-fork-pct=1 \ --max-sym-array-size=256 \ --libc=uclibc --posix-runtime ./gzip.bc -d --sym-files 1 100 and this is the output test cases i am getting (i am pasting just 2) : ktest-tool klee-last/test000031.ktest ktest file : 'klee-last/test000031.ktest' args : ['./gzip.bc', '-d', '--sym-files', '1', '100'] num objects: 5 object 0: name: 'A-data' object 0: size: 100 object 0: data: '\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\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\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 1: name: 'A-data-stat' object 1: size: 96 object 1: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff' object 2: name: 'stdin' object 2: size: 100 object 2: data: 'PK\x03\x04\x00\x00\x00\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\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\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 3: name: 'stdin-stat' object 3: size: 96 object 3: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff' object 4: name: 'model_version' object 4: size: 4 object 4: data: '\x01\x00\x00\x00' ktest-tool klee-last/test000013.ktest ktest file : 'klee-last/test000013.ktest' args : ['./gzip.bc', '-d', '--sym-files', '1', '100'] num objects: 5 object 0: name: 'A-data' object 0: size: 100 object 0: data: '\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\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\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 1: name: 'A-data-stat' object 1: size: 96 object 1: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff' object 2: name: 'stdin' object 2: size: 100 object 2: data: 'PK\x03\x04\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x80\x03\x00\x16\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\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 3: name: 'stdin-stat' object 3: size: 96 object 3: data: '\x01\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x92\x81\x00\x00\x01\x00\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\xecjOR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\x89\xa9UR\x00\x00\x00\x00\xff\xff\xff\x7f\xff\xff\xff\xff' object 4: name: 'model_version' object 4: size: 4 object 4: data: '\x01\x00\x00\x00'
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
