On 19/07/13 00:13, ANAS faruqui wrote:
I am trying to run KLEE on gzip. I want to generate test cases when one
parameter is always -d. So how do i give a concrete input while let the
others inputs be symbolic
The command i am using is :
klee --only-output-states-covering-new --libc=uclibc
Hi Jonathan,
Thanks for these three patches; nice catch with the last one.
There were again no commit messages going to klee-commits about your
patches; after some googling, I found out that commit messages
containing non-ASCII characters are discarded, see the thread below:
I recently added at http://klee.llvm.org/developers-guide.html a
developer's guide written by Dan Liew (thanks, Dan!). It currently only
discusses the build process and the testing infrastructure (and a couple
of misc items), so it would be great if other people would like to
expand it.
Thanks for the detailed info, Jonathan.
I agree that we could replace klee-libc with other code, but first of
all, I am wondering whether we still need it in the first place. My
impression is that everyone uses klee either standalone or with uclibc,
but please let me know if there are any
Hi Loi,
There is not reason not to have BFS in KLEE, and we would be happy to
add support for this: just send your patch for review to the
klee-commits mailing list.
This was never a priority because, as Paul mentioned, KLEE has more
advanced heuristics, including one that actively favors
Hi Urmas,
Those options are inherited from LLVM and don't affect the values
generated by KLEE through STP. (We need to reorganize the way KLEE
options are displayed; Dan Liew is currently looking into this.)
There is currently no support for generating the smallest or largest
possible
Hi Lei,
Thank you for your detailed instruction. Now we do like that. And,
another question, I think there are actually only 88 stand-alone
utilities in coreutils, unless considering false or test/[ as
stand-alone. I skipped dir, vdir, ginstall, groups, sha*sum,
false, and only test one of the
Hi Yi,
We used this sequence:
mkdir obj-klee
make -w O=obj-klee defconfig
cd obj-klee
make CC=klee-gcc LD=llvm-ld --disable-opt AR=llvm-ar SKIP_STRIP=y V=1
ln -s busybox_unstripped.bc toolname (for each tool you want to run)
You might need to adjust this a bit (I noticed that on my current
I want to work with examples that has float. Can KLEE deal with this?
KLEE cannot currently handle symbolic floating point expressions. A
fork KLEE called KLEE-FP can handle symbolic floating point
expressions. See http://www.pcc.me.uk/~peter/klee-fp/
Just a quick clarification: KLEE-FP has
On 08/02/13 13:48, Paul Rubel wrote:
Christian,
Cristian Cadar writes:
Hi Paul, I guess it would be useful to have more control over the LLVM
optimizations performed in KLEE. I would be happy to incorporate such a
patch.
This was a tricky question. It was posted to the klee list
On 08/02/13 14:44, Lei Zhang wrote:
So this means before replay a ktest, I should remove the old sanbox
directory and uncompress sandbox.tgz to create a new one, and then
copy the native utility compiled with gcov support to the new sandbox
directory and then reply the ktest?
Hi Lei, yes,
Hi Lei,
On 05/02/13 03:35, Lei Zhang wrote:
Coreutils experiment. They are very helpful! Now we have set up the
environment using Ubuntu 10.04 + LLVM 2.7 (I'd like to contribute to the
upgrading to 2.9 after I finish this project).
That would be useful, thanks.
And we have some
questions
Hi Paul, I guess it would be useful to have more control over the LLVM
optimizations performed in KLEE. I would be happy to incorporate such a
patch.
Best,
Cristian
On 31/01/13 15:29, Paul Rubel wrote:
Regarding optimizations I've been down that path lately. Even if the
code is compile
Hi, it's just, e.g., --with-llvm-build-mode=Release+Asserts.
Best,
Cristian
On 29/01/13 09:31, Alexandru Ionut Diaconescu wrote:
Hello everyone,
I was successfully able to install Klee on my LLVM 3.1 environment, but
it's not working properly. Then, I tried to install it on LLVM 2.9. I
have
this problem? I have searched a lot but didn't find any
useful information. Any advise is highly appreciated. Thank you in advance!
Best regards,
On Mon, Jan 21, 2013 at 3:19 PM, Cristian Cadar c.ca...@imperial.ac.uk
mailto:c.ca...@imperial.ac.uk wrote:
Hi Lei,
Here are the symbolic arguments
Hi Dilip,
Currently, KLEE has limited support for C++, and no support for
pthreads. However, there are certain extensions to KLEE that handle
these aspects, e.g., KLOVER for C++ and Cloud9 for pthreads. Take a
look at http://klee.llvm.org/Publications.html for more information.
Cristian
Hi all,
To make it easier for people who try to reproduce our OSDI'08
experiments, I have decided to put together a web page with some
additional details:
http://klee.llvm.org/CoreutilsExperiments.html
Best,
Cristian
___
klee-dev mailing list
Hi, most likely you have not compiled all libraries used by vim to LLVM
bitcode.
Best,
Cristian
On 16/01/13 01:31, 李永超 wrote:
Hi Everyone:
I have been trying to run vim trough klee and generate test cases.
Having built vim with llvm, I run following command to run it with klee:
klee
Hi Lei,
Our choice was based on a high-level understanding of the Coreutils
apps: most behavior can be triggered with no more than 2 short options,
1 long option, and 2 small files (one of which is stdin).
Best wishes,
Cristian
On 14/01/13 14:58, Lei Zhang wrote:
Hi All,
We are working
I recently pushed a few patches by Tomasz Kuchta (thanks!) which add the
following useful features to KLEE:
1) The ability to log only the queries that time out, or are taking
above a certain specified threshold. It is often too expensive to log
all the queries, and this new feature
Hi all,
We are sorry that the KLEE mailing lists were down during the last few
days; the problems were caused by some unexpected hardware failures.
We have decided to move this list from klee-dev@keeda.stanford.edu to
klee-...@imperial.ac.uk. You will soon be receiving a message saying
(e.g., cd test/Feature;
../TestRunner.sh/ExprLogging.c).
Thanks,
Cristian
On 20/11/12 10:34, Cristian Cadar wrote:
Hi Bogdan,
KLEE currently supports LLVM 2.9. I never tried a more recent version,
but I'm glad to hear that at least it compiles; I can take a look at the
test failures at some
Hi Bogdan,
KLEE currently supports LLVM 2.9. I never tried a more recent version,
but I'm glad to hear that at least it compiles; I can take a look at the
test failures at some point, although I don't think I'll have time to do
so very soon.
Best,
Cristian
On 19/11/12 20:02, Bogdan Copos
Hi all,
I've just pushed several patches by Dan Liew (thanks, Dan!) which add to
KLEE the ability to output queries in the standard SMT-LIB language (see
http://www.smtlib.org/ for more info on SMT-LIB). This makes it easy to
debug queries outside KLEE, and to quickly see how other SMT
Hi Stephan,
Sorry, I forgot to add that file when I committed the last patch. It's
solved now.
Cristian
On 19/10/2012 08:26, Stephan Falke wrote:
Hi,
KLEE trunk currently doesn't compile:
In file included from STPBuilder.cpp:10:
STPBuilder.h:14:37: error: klee/util/ArrayExprHash.h: No
Hi Andrei, thanks for your message. I have now updated the installation
instructions and added a link to your post. BTW, I also had to set
CPLUS_INCLUDE_PATH to /usr/include/i386-linux-gnu in order to
successfully install KLEE on Ubuntu 12.04.
Best,
Cristian
On 10/09/12 10:43, Porumb Andrei
Hi Dan,
Thanks for your message. I agree with your fixes to getTrue() and
getFalse(); I applied your patch in r163606:
http://llvm.org/viewvc/llvm-project?rev=163606view=rev
Regarding ConstantExpr::getZExtValue(), I think the current version is
correct. The bits argument simply states the
Hi,
The STP version in the repository is really old, from 2009. I plan to
remove that directory soon and make --with-stp required when configuring
KLEE. Would anyone like to update the configure script accordingly?
It should be fine to use a newer version of STP; we mention r940 on the
Hi, STP can handle non-linear constraints, although they are typically
more expensive to solve.
Cristian
On 05/13/2012 04:21 PM, Xiaomei Hou wrote:
Dear KLEE project members:
STP constraints solver can not solve nolinear constraints, according to
its capacity. Klee is depend on STP. Why can
Hi Lionel,
Each call to klee_make_symbolic() creates a new symbolic object, which
is completely unconstrained. I hope this clarifies KLEE's behavior on
this program.
Best,
Cristian
On 04/24/2012 04:01 PM, Lionel PRAT wrote:
Hi,
I find it hard to understand, why in the example below, klee
Hi Daniel,
KLEE requires a constraint solver with support for the theory of
bitvectors and arrays of bitvectors, i.e. QF_ABV in SMT-LIB:
http://goedel.cs.uiowa.edu/smtlib/logics/QF_ABV.smt2
I am not sure whether Yices implements this theory or not, but several
other solvers do. For example,
On 11/20/2011 10:33 AM, Gang Hu wrote:
The memory leak is caused by two reasons.
First, the MemoryObject objects are not freed, until the MemoryManager
is destroyed. Second, when KLEE allocates a non-fixed MemoryObject
object, KLEE also allocates a block of memory which is the same as the
Hi Paul, arrowdodger,
Thanks for your help diagnosing and fixing this issue. Please see r146350:
http://llvm.org/viewvc/llvm-project?view=revrevision=146350
Best,
Cristian
On 16/08/2011 10:00, arrowdodger wrote:
On Sun, Aug 14, 2011 at 9:06 PM, Paul Marinescu
paul.marine...@imperial.ac.uk
Hi Ben,
Thanks for your patches. I already pushed a few of your changes here:
http://llvm.org/viewvc/llvm-project?view=revrevision=146352
http://llvm.org/viewvc/llvm-project?view=revrevision=146353
A few comments about your other changes:
(1) RUSAGE_SELF: you should send this patch to the STP
Hi, we are always interested in patches for KLEE, which you can send to
this mailing list. There is also a list of open projects at
http://klee.llvm.org/OpenProjects.html.
Best,
Cristian
On 14/11/2011 00:56, Zhang Yufeng wrote:
Hi, how do you manage your project when developing KLEE?
I am
Hi,
The STP input language used by the .cvc files is documented here:
http://sites.google.com/site/stpfastprover/stp-documentation
The PC language used by the .pc files is documented here:
http://klee.llvm.org/KQuery.html
Best,
Cristian
On 03/11/11 15:00, amitaï madar wrote:
Hi all.
I want
Hi, you will need to download the svn version and compile KLEE and LLVM
in debug mode. If more people would like this, we can also create a
CDE package with a debug build, although the main goal of the CDE
package is just to quickly try KLEE, and not to do any development work.
Best,
Cristian
Yes, the tutorial was generated using an earlier version of LLVM (2.8).
I will change it to a new tutorial that does not interact with these
latest optimizations.
Best,
Cristian
On 27/09/11 10:34, Martin Nowack wrote:
Hi Kevin, depending on the version of LLVM you use, nothing is
wrong.
Applied in r132786, thanks.
Cristian
On 09/06/11 11:52, arrowdodger wrote:
On Wed, Jun 1, 2011 at 4:18 PM, arrowdodger 6yearold at gmail.com
mailto:6yearold at gmail.com wrote:
Hello. Here is a quick fix for FreeBSD build.
___
On 07/06/2011 23:40, Vijay Ganesh wrote:
On Tue, Jun 7, 2011 at 5:38 PM, Cristian Cadar
c.cadar at imperial.ac.uk mailto:c.cadar at imperial.ac.uk wrote:
On 07/06/2011 12:12, Russell Wallace wrote:
I notice Klee chose STP for its SMT solver. I'm curious as to the
reason for this choice
Hi Milen,
I think this should work fine if you run KLEE with uclibc support.
Best,
Cristian
On 23/05/11 22:58, Milen Dzhumerov wrote:
Hi all,
I've come across the observation that KLEE doesn't properly handle the return
of statically allocated memory regions returned by calls to external
Hi Philip,
Thanks a lot for the CDE package, it's really helpful. I just added
your instructions to the Getting Started webpage.
Best,
Cristian
On 26/05/2011 00:42, Philip Guo wrote:
With the help of Cristian, I've put together an improved version of the
Klee package:
Hi, did you manage to sort this out? This large number of test failures
is usually due to using incompatible llvm-gcc and llvm versions. Make
sure you download the right binary for llvm-gcc 2.7 (should be
http://llvm.org/releases/2.7/llvm-gcc4.2-2.7-x86_64-linux.tar.bz2 in
your case), put
On 18/04/2011 17:55, arrowdodger wrote:
I've solved problem with kleaver parser. With this patch `make test` yields:
# of expected passes 84
# of unexpected failures 2
# of expected failures 1
XFAIL: /home/arr/projects/klee/test/Expr/Evaluate2.pc
FAIL:
On 23/04/2011 21:02, Peter Collingbourne wrote:
On Sat, Apr 23, 2011 at 08:47:45PM +0100, Cristian Cadar wrote:
On 18/04/2011 17:55, arrowdodger wrote:
I've solved problem with kleaver parser. With this patch `make test` yields:
# of expected passes 84
# of unexpected failures 2
Hi all,
We decided to add a webpage to the KLEE website listing
projects/papers that use or extend KLEE. Please let me know if there
are any additional papers that we should list!
http://klee.llvm.org/Publications.html
Best,
Cristian
Hi Sree,
There is no support for doing this from the command-line, but you can
restrict the symbolic arguments to only contain digits by adding some
calls to klee_assume() in klee_init_env.c.
Best,
Cristian
On 10/10/10 16:46, Sreekumar Kodakara wrote:
Hi,
First of all, thanks for creating
Hi Xiao,
1. In the tutorials, only klee_make_symbolic_name and klee_make_symbolic
are used, where can I find the other methods such as klee_int you
mentioned? Any documentation on how to use these methods?
You can find the entire list of KLEE intrinsics, with comments, in
On 01/09/10 19:44, Bueno, Denis wrote:
On Sep 1, 2010, at 11:15 AM, Cristian Cadar wrote:
Hi Denis,
The non-deterministic behavior that you see in your runs is most likely
caused by the addresses returned by malloc(). I think there was a
previous thread on the list which discussed
, so it is better to stop. I modified the patch.
Cristi
On Jul 16, 2010, at 8:19 PM, Cristian Cadar wrote:
Hi Cristi,
That's a good patch. I'm just wondering if there's really any
benefit of continuing execution once KLEE runs out of file descriptors
looks fine.
Since several people ran into this problem, perhaps it is better to also say
in the message to klee_error something like try to increase your file
descriptors limit.
Cristi
On Aug 5, 2010, at 11:39 AM, Cristian Cadar wrote:
Hi Cristi,
That's a rather minor thing, but instead
Hi, it would be indeed useful to set up a bigger regression suite which
would make sure that KLEE still finds the bugs in Coreutils. So it
would be great if anybody would offer to do this.
However, to reproduce the bugs, I would recommend trying the KLEE and
LLVM versions from the time of
Thanks, Peter. I think it's a very useful patch: it still allows us to
use the more stable internal STP, as well as more recent versions of
STP, including the svn one.
Best,
Cristian
On 09/07/10 16:24, Peter Collingbourne wrote:
Hi Daniel,
Sorry for the slow response.
On Thu, Apr 08,
$ klee-replay --create-files-only klee-last/test70.ktest
make_symbolic mismatch, different sizes: 6 in input file, 4 in code
With -sym-args 2 3 5 exactly the same klee-reply command seems to work
(certainly it creates a file).
Is this a bug that I should drop into Bugzilla or is
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
Sorry for the misunderstanding. I just wanted to make sure that you
used the --with-llvm option. But since you compiled KLEE successfully,
you are facing a different problem. Looking at your 'make check' output
closer, I see llvm-gcc does not seem to be in your PATH. Maybe you
forgot this
Hi Jun,
As far as I can tell, there's a configuration problem there. You should
make sure that you passed the --with-llvm option to KLEE's configure
script.
Cristian
On 16/04/10 16:17, Jun Koi wrote:
Hi,
I am starting to play with Klee. I followed the instruction on the
homepage to
On 14/04/10 18:54, Thanh Vo wrote:
Hi Cristian,
Thank you again for your answer. I just fixed the input program and make
symbolic to the variables. But, the problem remains because STP then
Klee does not support floating point numbers. I also noticed that STP
does support real arithmetic.
Hi Stefan,
The invariant you mention should indeed hold. I've never seen a
violation on a 32-bit machine. But I encountered a similar issue on
64-bit, where I think the next address should have been none. I don't
have time to debug this any further, but let me know if you do.
Best,
In my case, the klee only generates one path and one test. How many
paths and tests that the test generator should generate for my program?
( I think it should be 32).
Hi Thanh, since you're not marking anything as symbolic, there is only
one path through the program, as in a normal
Hi Vladimir,
Just ignore for now the patch for LLVM 2.7:
svn co -r 98465 http://llvm.org/svn/llvm-project/klee/trunk klee
Cristian
On 23/03/10 04:48, Vladimir G. Ivanovic wrote:
on 03/13/2010 09:36 PM Daniel Dunbar said the following:
I just checked in a patch for building KLEE with LLVM
Hi Raimondas, this is really a question of how LLVM compiles the code.
In the first case, LLVM lifts the call to klee_warning before the second
if statement, while in the second case it doesn't. You can take a look
at klee-last/assembly.ll, which contains a disassembled version of the
actual LLVM
Hi Tony,
I'm cc-ing the klee-dev mailing list, as other people might be able
to help and/or benefit from this exchange.
I always use a binary release of llvm-gcc, so I have no experience
compiling it. I had problems compiling LLVM with certain gcc
compilers. This
201 - 263 of 263 matches
Mail list logo
