Mr. Cadar, thanks so much for your advice. I later used the exact r165499 version(we personally changed it a bit, although it's really trivial), and compiled coreutils bitcode without any optimizations(seems that the default is -O2) they linked as klee-gcc does(llvm-ld), then I didn't see such external functions in the cases I used before(it's weird, really).
Also, thanks for the extra information and I'll open an issue when I meet this issue once more. Thanks, Hongxu Chen On Fri, Nov 8, 2013 at 7:10 PM, Cristian Cadar <[email protected]>wrote: > 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
