[klee-dev] concretized symbolic size

2010-05-02 Thread Cristian Zamfir
I sometimes see states terminated with the error message concretized symbolic size. Since this produces a test*.err file in Klee's output, I assumed it could be related to a possible bug found by Klee. However, when reading the source code in Executor::executeAlloc() I see that in case a large

[klee-dev] re-enable inline asm warnings

2010-05-02 Thread Cristian Zamfir
This should re-enable inline asm warnings. Cristi --- main.cpp(revision 102872) +++ main.cpp(working copy) @@ -807,7 +807,7 @@ for (Function::const_iterator bbIt = fnIt-begin(), bb_ie = fnIt-end(); bbIt != bb_ie; ++bbIt) { for (BasicBlock::const_iterator it =

[klee-dev] problem when building coreutil

2010-05-02 Thread Daniel Dunbar
Hi Wenbin, It doesn't look like KLEE is configured with the right uclibc path, at least the path it is constructing for libc.a looks bogus (/lib/libc.a). - Daniel On Tue, Apr 20, 2010 at 7:47 PM, Wenbin Zhang zhangwen at cse.ohio-state.edu wrote: Hi all, I?m new to klee and trying to build

[klee-dev] KLEE 2.7

2010-05-02 Thread Daniel Dunbar
Fixed in r102873, thanks for the report! FWIW, I hope to have a buildbot up real soon now... - Daniel On Fri, Mar 19, 2010 at 8:54 AM, Cristian Cadar c.cadar at imperial.ac.uk wrote: Hi Daniel, After pulling these changes, I don't get debug info anymore. ?In particular, WriteCov and

[klee-dev] KLEE 2.7

2010-05-02 Thread Daniel Dunbar
Hi Vladimir, On Mon, Mar 22, 2010 at 9:48 PM, Vladimir G. Ivanovic vladimir at acm.org wrote: on 03/13/2010 09:36 PM Daniel Dunbar said the following: I just checked in a patch for building KLEE with LLVM 2.7. I have tested it on Linux x86_32 with LLVM 2.6 and 2.7 and on Darwin x86_32 and

[klee-dev] Fail on make check

2010-05-02 Thread Daniel Dunbar
You shouldn't need to compile llvm-gcc yourself, I don't do this on Linux. Make sure that your LLVM found llvm-gcc when it was configured though, it should be in the configure output. - Daniel On Fri, Apr 16, 2010 at 9:56 PM, Jun Koi junkoi2004 at gmail.com wrote: On Sat, Apr 17, 2010 at 8:39

[klee-dev] More modern uClibc?

2010-05-02 Thread Cristian Cadar
Hi, I just added a link on the KLEE webpage to a version of uclibc that incorporates the changes needed to compile it on x64, which Cristian Zamfir kindly agreed to share with everybody. Let us know if there are any issues with this version, and whether it also works on 32 bit, in which case

[klee-dev] KLEE 2.7

2010-05-02 Thread Shaul Kedem
Hi, I've tried running make check on the latest svn and it doesn't seem to work, but the make unittests does... here is the output (warning, very long) : [shul at localhost klee]$ ./configure --with-llvmsrc=../../llvm-2.7 --with-llvmobj=../../llvm-2.7 checking build system type...

[klee-dev] KLEE 2.7

2010-05-02 Thread Daniel Dunbar
Hi Shaul, It looks like llvm wasn't able to find an llvm-gcc compiler when you configured it. You need to install or build llvm-gcc, and pass extra options to LLVM's configured if it isn't in your path. - Daniel On Sun, May 2, 2010 at 3:15 PM, Shaul Kedem shaul.kedem at gmail.com wrote: Hi,

[klee-dev] Fail to compile klee

2010-05-02 Thread Daniel Dunbar
Hi Jun, Are you sure that you are using an llvm-gcc from the 2.6 release? - Daniel On Thu, Apr 22, 2010 at 8:06 AM, Jun Koi junkoi2004 at gmail.com wrote: Hi, I tried to compile klee on Ubuntu 10.4 (with llvm-2.6), and got below errors. How can I fix that? (The klee is latest code