Hi Hongxu,
You would need to debug the __overflow issue; could you also open an
issue on GitHub?
It is important to read the info on that webpage and follow the
instructions there. Coverage numbers were obtained using replay+gcov,
as mentioned in the paper. (The KLEE stats are at the level of bitcode,
and also refer to library code.) Lei Zhang submitted a useful patch
that makes replaying easier; I still need to review it, but you can find
it at https://github.com/ccadar/klee/pull/31. There are also other
issues to take care when using gcov -- e.g, gcov doesn't record coverage
on _exit -- which might require small adjustments.
Cristian
On 05/11/2013 10:00, Hongxu Chen wrote:
Hi,
I'm trying to reproduce the coreutils results in klee08 paper(klee
"make check" has been passed).
We were following KLEE "Coreutils Experiments"
page(http://ccadar.github.io/klee/CoreutilsExperiments.html). And the
major variants are:
1. used KLEE svn r165499 rather than revisions before r161056, and I got
STP from KLEE "Getting Started"
page(http://ccadar.github.io/klee/GetStarted.html).
2. used coreutils-6.10 rather than 6.11.
3. didn't use "--environ=test.env" and "--run-in=/tmp/sandbox"; also
customized a "--output-dir" option. (I guess these are really trivial
changes)
The 89 cases are running on a x86_64 machine whose OS is ubuntu12.04
LTS. And here is some extra information about it:
1. > sudo fdisk -l
Disk /dev/sda: 250.0 GB, 250000000000 bytes
255 heads, 63 sectors/track, 30394 cylinders, total 488281250 sectors
Units = sectors of 1 * 512 = 512 bytes
Sector size (logical/physical): 512 bytes / 512 bytes
I/O size (minimum/optimal): 512 bytes / 512 bytes
Disk identifier: 0x00039844
Device Boot Start End Blocks Id System
/dev/sda1 * 2048 480026623 240012288 83 Linux
/dev/sda2 480028670 488280063 4125697 5 Extended
/dev/sda5 480028672 488280063 4125696 82 Linux swap / Solaris
2. > grep "model name" /proc/cpuinfo
model name : Intel(R) Core(TM)2 CPU 6400 @ 2.13GHz
model name : Intel(R) Core(TM)2 CPU 6400 @ 2.13GHz
We ran the cases for 3 times, and it took several days(sorry I didn't
get the exact hours); I noticed some results with the help of
"klee-stats --print-all" for each case:
1. There are several "*.external.err", and the failed external calls are
"__overflow" and "__uflow". they both result from
"/usr/include/bits/stdio.h" of Line 66, however I didn't find any
defitinition of them.
2. For those cases that KLEE halts without any external function fail, I
find KLEE halt mainly because they are timed-out(I infer this since the
"Time" results are typically a bit larger than "3600"). Should I
increase the "--max-time" number?
3. The *ICov* and *BCov* I run isn't quite high(the highest are about
45% and 35% respectively). Should I trust the statistics or I am using
the wrong results?
4. "TSolver" still occupies most of the time(most of them are above 98%
and the lowest is 95.23%).
I believe I must have missed something and might have configured
incorrectly.
So I really need your kind help; any advice will be appreciated, thanks
in advance!
Best Regards,
Hongxu Chen
_______________________________________________
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
