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
