On Fri, Jan 29, 2010 at 1:50 PM, David B Lightstone <david.lightstone at prodigy.net> wrote: > Reply within body > > Dave Lightstone > >> -----Original Message----- >> From: daniel.dunbar at gmail.com [mailto:daniel.dunbar at gmail.com] On >> Behalf > Of >> Daniel Dunbar >> Sent: Friday, January 29, 2010 11:11 AM >> To: david.lightstone at prodigy.net >> Cc: klee-dev at keeda.stanford.edu >> Subject: Re: [klee-dev] FW: Completeness of generated test cases >> >> On Wed, Dec 30, 2009 at 3:57 AM, David B Lightstone >> <david.lightstone at prodigy.net> wrote: >> > I have started to play with Klee to see what it does, to see its limits >> > >> > The test problem which I choose to apply third was >> > >> > int test(int a) >> > { >> > ? if (( a < 1) && (a > 1)) >> > ? ? ?return 1; >> > ? else >> > ? ? ?return 0; >> > } >> > >> > >> > There is no value of a for which the condition is true, so path coverage > is >> > impossible. >> > >> > A good optimizing compiler probably would have reduced the code to >> > ?return (0); >> > I did not compile with optimization enabled >> > I used --emit-llvm -c -g for the compile options >> > I used --only-output-states-covering-new -optimize for the klee options >> >> In the version of LLVM that KLEE currently uses, having debugging >> information dramatically inhibits optimization. Try removing the "-g" >> when compiling. If you still see two test cases, please send me a .tgz >> with the contents of the klee-last directory. > > Phenomena correlated to the -g option > I think it will be advantageous to use common scripts for purposes of > problem reports. This if only to avoid context interpretation problems. > (i.e. which options are in play). That way things can be more readily > characterized to the options selected. > > Henceforth I am using for compiles (adjust path to klee root for library > files as appropriate) > llvm-gcc --emit-llvm -c ?-B /home/dbl/Tools-Source/llvm/klee/klee $1 -o > ${1%.*}.o
Yes, unfortunately compiling code for klee turns out to be one of the most annoying parts of trying klee. Fortunately, with the rapid development of Clang (http://clang.llvm.org) we are now in a much better position to make this easy, however I have very little time to do work on KLEE these days (unfortunately). - Daniel > Henceforth I am using for KLEE execution (klee assumed to be in path) > klee --only-output-states-covering-new $1 > > > >> >> > The generated test cases were >> > a = 0; >> > a = 2; >> > >> > (1) It is not clear what the Klee -optimize option achieves. Certainly > it is >> > not code optimization. Were that the case the impossibility if achieving > the >> > TRUE path would have been discovered symbolically. I suspect that > somewhere >> > there is a declaration of intent for each of the options. I have yet to >> > actually look for it. If such a declaration does not yet exist, best to >> > write one. >> >> Yes, we certainly need more documentation on the KLEE options. Have you > seen: >> ? http://klee.llvm.org/TestingCoreutils.html >> Currently it has the most content on how to use KLEE and explains some >> of the options. > > Yes > >> >> ?- Daniel >> >> > >> > >> > dbl >> > >> > >> > >> > >> > _______________________________________________ >> > klee-dev mailing list >> > klee-dev at keeda.stanford.edu >> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> > >> > _______________________________________________ >> > klee-dev mailing list >> > klee-dev at keeda.stanford.edu >> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> > > >
