Yes, but the object 2 is listed as 'stdin' while the only variable is considered is the symbolic file A. which is still all zeros. Therefore I am confused, which one to refer to as we are not giving input through 'stdin'.
On Sat, Oct 12, 2013 at 12:40 AM, Urmas Repinski <[email protected]>wrote: > Hello, > > The thing is that those two test cases are not all zeros and not the same - > > They are different at object2 variable's values, and x08 corresponds to > the character with ASCII code '8', those are strings 100 character long as > it were necessary to generate: > --sym-files 1 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' > > > and > > 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' > > I see no error, > and if inputs are in the wrong format, then probably you should modify > parameters. > > Urmas Repinski. > > > ------------------------------ > From: [email protected] > Date: Fri, 11 Oct 2013 20:14:04 -0400 > To: [email protected] > Subject: [klee-dev] KLEE with Gzip > > > 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
