Hi,
I have two linking problems.
The first one is when compiling a program that uses sockets. In my
case, it should be OK if the socket calls/syscalls are executed as
external functions, however, I get this error message:
KLEE: WARNING: undefined reference to function: __socketcall
.
.
.
Hi Cristian,
On Sat, Feb 7, 2009 at 5:38 PM, Cristian Zamfir cristian.zamfir at epfl.ch
wrote:
Hi,
I have two linking problems.
The first one is when compiling a program that uses sockets. In my
case, it should be OK if the socket calls/syscalls are executed as
external functions,
Hey Philip,
using the standard LLVM toolchain, is there an easy way to make a static
symbol 'non-static'? i have a bunch of static functions that i want to
essentially make non-static, without having to resort to re-writing the
source. thanks!
what are you trying to do that needs that?
thanks dawson and daniel for the quick answers ... i found a workaround and
no longer need to resort to that grossness. nevermind!
On Sun, Feb 15, 2009 at 9:12 PM, Dawson Engler engler at
csl.stanford.eduwrote:
Hey Philip,
using the standard LLVM toolchain, is there an easy way to make a
when i try running 'make regress' in klee/, it doesn't work at all. all it
seems to do is to go into klee/regression and run 'make' in there. is that
a regression suite that you guys have been actively maintaining, or is it
deprecated? thanks.
there are lots of errors of the following form:
$
reads and writes, so the code sequence
--
a[i] = 10;
a[0] = 2;
x = a[j]
--
would translate to something like Read(Write(Write(a, i, 10), 0, 2),
j). STP has various tricks to try and make the solving of such
expressions more efficient, but in general these expressions are
expensive (they transform
Pedantically:
unsigned a,b,c,d;
I assume you mean int; undefined overflow is perfectly well defined in
C99 (6.2.5p9, if you are bored).
No, I mean unsigned.
I'm not looking for overflow errors. I just want to assert they don't
happen.
Ultimately, the front-end would have to
h, i don't know of a good methodical way to debug this. one idea is to
try to run with the following 2 options:
--write-cov (this will write a .cov file for each terminated state with the
file/line info for any *new* lines that state has covered that previous
states haven't ... make sure you
Hi Phil,
On 26.03.2009, at 06:06, Philip Guo wrote:
--write-cov (this will write a .cov file for each terminated state
with the file/line info for any *new* lines that state has covered
that previous states haven't ... make sure you compile your app with
-g debug info to get file/line
let's say we have a complex arithmetic expression. is there a simple
clean way to assert that no intermediate results (subexpressions)
contain an overflow?
e.g., if we have
unsigned a,b,c,d;
a+b+c+d
i'd like to assert that a+b+c+d does not overflow. however i'm worried
that
Some more details, Chris explained that this is to support the MSVC
pragmas which allow code to specify which libraries are used. It is
possible in this case that they are just slipping in by accident, I
wonder if things work if you just disable the assertion?
- Daniel
On Fri, May 8, 2009 at
Yes, the llvm.org has been fairly slow recently, this is currently
being worked on and will be fixed soon I hope.
- Daniel
On Mon, Jun 1, 2009 at 8:32 PM, Dharmalingam Ganesan
dganesan at fc-md.umd.edu wrote:
Hi,
Thanks for the release. Often, unable to connect to http://klee.llvm.org
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
could be useful for writing future FT-Apps related scripts :)
http://pythonpaste.org/scripttest/
-- next part --
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090608/110bb954/attachment.html
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,
That's great, thanks for sharing the newest Uclibc! I was actually using
some old code in runtime/POSIX that used 'klee_make_symbolic_name', so I
updated to the latest versions of LLVM and KLEE. However, now I'm
running into some other problem when running coreutils, linking uclibc
and
Thanks Daniel and Cristian;
i tried with the current version of llvm (svn co
http://llvm.org/svn/llvm-project/llvm/trunk llvm )
and llvm-gcc4.2-2.5. However still getting same error:
llvm[2]: Compiling Debug.cpp for Release build
llvm[2]: Compiling main.cpp for Release build
main.cpp: In
Hi Stefan,
This should be fixed in TOT, thanks.
- Daniel
On Fri, Jul 17, 2009 at 6:56 AM, Bucur Stefanstefan.bucur at epfl.ch wrote:
Hello,
I'm having an issue with running the latest snapshot of KLEE (together with
the latest snapshot of LLVM): everything builds properly, as instructed
Hi all;
I am trying to run klee with llvm 2.4 and llvm-gcc 2.5 with OS ubuntu 8.10
(as given in http://klee.llvm.org/GetStarted.html), however i am getting an
error, given below,
when i am trying to build klee with make ENABLE_OPTIMIZED=1 :
llvm[2]: Compiling Debug.cpp for Release build
llvm[2]:
Hello Daniel,
Thanks for applying our patches, it is much easier to work when they
are in the mainline.
On Mon, Aug 3, 2009 at 10:14 AM, Daniel Dunbardaniel at zuster.org wrote:
Hi all,
I thought I would mention a few bits of recent KLEE news...
1. KLEE now works on x86_64 on Linux. Many
On Tue, Aug 4, 2009 at 3:25 AM, Vladimir Kuznetsovks.vladimir at gmail.com
wrote:
Hello,
What is the easiest way to replay tests with symbolic arguments and symbolic
files ? It seems that libkleeRuntest.so is not handling them. One way would be
to parse .ktest file and manually invoke a
Hello Daniel,
Thank you for the explanation. Could you please give a hint how soon the tool
will be published ? I am a bit in rush, so I want to decide whether to wait or
to implement something more simple for now myself.
--
With the best regards,
Vladimir Kuznetsov
On Tuesday 04 August 2009
On Tue, Aug 4, 2009 at 11:56 AM, Vladimir
Kuznetsovks.vladimir at gmail.com wrote:
Hello Daniel,
Thank you for the explanation. Could you please give a hint how soon the tool
will be published ? I am a bit in rush, so I want to decide whether to wait or
to implement something more simple for
Hello Cristian,
I have solved this problem by disabling UCLIBC_HAS_XLOCALE. All changes that I
have made to uClibs configuration and source code in order to compile it on
x86-64 are in the attached file.
On Sunday 23 August 2009 02:44:54 Cristian Zamfir wrote:
Hi,
I am trying to compile
Thanks Vova. Indeed, I made the other changes without disabling
UCLIBC_HAS_XLOCALE. Now it works.
I am still wondering what are the changes from the regular uclibc, in
case similar problems appear in the future.
We can also try to find them out from the diff, but I am not sure
which uclibc
Hi Jiri,
It builds with trunk for me, what problem are you seeing?
- Daniel
On Mon, Sep 7, 2009 at 2:27 AM, Jiri Slabyjirislaby at gmail.com wrote:
Hello,
which llvm revision exactly you build klee against? It doesn't build
against the llvm trunk anymore. Thanks.
Hi Milena,
On Sun, Sep 27, 2009 at 1:41 PM, Milena Vujosevic-Janicic
milena at matf.bg.ac.rs wrote:
I am a PhD student at the University of Belgrade,
working in software safety. I have downloaded your
tool Klee and ran it successfully on a range of
examples.
Cool!
I am planing to try to
Hi Suhabe,
This is what the klee-replay tool is for. See:
http://klee.llvm.org/TestingCoreutils.html
for a tutorial that covers all the necessary steps.
- Daniel
On Mon, Oct 12, 2009 at 3:41 AM, Suhabe Bugrara suhabe at stanford.edu wrote:
Thanks for the reply.
It looks like using these
Hello,
On a particular machine I use (cluestick), the STP solver has been
timing out frequently, even with a long timeout such as 10 minutes.
An investigation into this problem reveals that the 'for (;;)' loop
in MINISAT::Solver::search, located in $KLEE_ROOT/stp/sat/Solver.C,
loops
Hi Zhi,
Please see the tutorial here, it should explain this:
http://klee.llvm.org/TestingCoreutils.html
Cheers,
- Daniel
2009/10/14 Zhi, Shen zong_y365 at 163.com:
Dear All,
I want to run some testcases on
coreutils(http://www.gnu.org/software/coreutils/) while the linking problem
Hi,
I am trying to reproduce the bugs from the OSDI paper.
I managed to reproduce 7 bugs on the native binaries: using the
instructions in the paper, it worked for paste, mkdir, mknod, mkfifo,
tac, seq and ptx -F\\ abcdefghijklmnopqrstuvwxyz
There are 3 bugs I cannot reproduce with the
hello,
I follow the instructions on Getting Started page, but encounter problems
when configure llvm. what is the version of this llvm? are there any special
requirements to configure it?
-- next part --
An HTML attachment was scrubbed...
URL:
Hi,
Here are the steps I went through to compile klee on an AMD quad
x86_64 with fedora core 11:
(see comments at the end)
1. create 3 dirs: llvm-gcc, llvm and klee in $HOME. (if you want to
check where your $HOME points to, write 'echo $HOME' in a terminal
window)
2. download llvm-gcc 2.6
hello,
thanks a lot for your emails. i compile klee on an intel core 2 Duo with
Fedora 11. i use llvm-gcc-4.2-2.6-i686-linux.tar.gz according to my computer
configuration. others are the same. i follow your instructions to build
klee, but i encounter questions.everything is fine until step 11
On Sun, Feb 7, 2010 at 5:27 PM, lokesh agarwal
lokesh.agarwal1986 at gmail.com wrote:
Hey everyone,
I was trying to work out how exactly klee handles symbolic files.
So i looked into the definition of the __fd_open() call stub, in
runtime/POSIX/fd.c
This is what I could make out:
The code
Thanks for the fix Stefan, I applied it in r95659.
- Daniel
On Thu, Feb 4, 2010 at 10:22 AM, Stefan Bucur stefan.bucur at epfl.ch wrote:
Greetings,
I recently posted on Bugzilla a bug report [1] concerning the crash of
Klee 64-bit during symbolic memory allocation, for a certain number of
Hi Stefan,
I don't understand parts of this patch. It shouldn't be necessary to
force KLEE to compile with -std=c++0x?
- Daniel
On Fri, Jan 29, 2010 at 10:37 AM, Stefan Bucur stefan.bucur at epfl.ch wrote:
Greetings,
As I had some issues during Klee compilation process on Ubuntu 9.10,
I'm
Hi,
I switched to using klee-replay instead of setting the env, and now the test
case seem to run correctly, but I'm a bit confused by some of the output.
test case:
#include stdlib.h
#include string.h
#include fcntl.h
#include unistd.h
void func(char *userInput) {
char arr[8];
From: Peter Collingbourne pc...@doc.ic.ac.uk
This patch results in a small decrease in binary size (debug build
x86_64: ~3000 bytes for klee and ~1 for kleaver).
---
include/klee/Expr.h |2 +-
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/include/klee/Expr.h
I am considering using Klee for analyzing Java code and I have a question
regarding
the feasibility of this. The reason why I am considering this is that it
seems like Klee
can take any llvm bytecode as input. VMKit is capable of producing llvm
bytecode for
java, which is what llvm-gcc produce as
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100303/775447ba/attachment.html
Hello,
I just enjoyed the OSDI 2008 paper about KLEE. I hope this list is a good
place to ask questions about it!
Footnote 9 caught my attention because it suggests that the way KLEE lays out
its state representations in memory affects the results of the run. But if I
write code like
On Sat, Mar 6, 2010 at 3:38 PM, Chung-chieh Shan ccshan at rutgers.edu wrote:
Hello,
I just enjoyed the OSDI 2008 paper about KLEE. ?I hope this list is a good
place to ask questions about it!
Sure!
Footnote 9 caught my attention because it suggests that the way KLEE lays out
its state
Hi,
Currently, when testing the printf tool from coreutils, Klee will hit an assert
in ConstantExpr::fromMemory because it does not handle X86_FP80TyID (80 bit
float).
Adding support for this seems like it requires quite a few changes:
- adding support for the 80 bit float type in Expr.h
-
Hi Cristi,
I submitted a patch for this to klee-commits... Waiting for Daniel to commit it.
-David
--Original Message--
From: Cristian Zamfir
Sender: klee-dev-bounces at keeda.stanford.edu
To: klee-dev at keeda.stanford.edu
Subject: [klee-dev] support for X86_FP80TyID
Sent: Mar 11, 2010
On Thu, Mar 11, 2010 at 11:38 AM, Jonathan Cooke jdcooke at andrew.cmu.edu
wrote:
Hello,
I'm attempting to modify the constraints KLEE adds to states in hopes of
getting better path merging. ?I noticed when KLEE comes across an
assignment, rather than adding a constraint about the variable
On Thu, Mar 11, 2010 at 4:38 PM, David A. Ramos davidramos at stanford.edu
wrote:
Hi Cristi,
I submitted a patch for this to klee-commits... Waiting for Daniel to commit
it.
My tentative plan is to get this in this weekend, as well as the 2.7 patches.
- Daniel
-David
--Original
Hello,
While testing the expr coreutil, I ran into a Klee crash caused by
LLVM instructions processing 128bit integers (i128 types).
Surprisingly enough, they can be found in various places in the LLVM
assembly generated by LLVM on a 64-bit architecture, as optimization
tricks when passing large
Ahh, I was thinking the constraints passed to the solver held per-line
information rather than per-CFG block information. I was wondering why
there weren't constraints for the contents of each variable in the
constraint vector but I see now that would be unnecessary.
Thanks,
Jonathan
Daniel
Daniel,
Are the changes backwards compatible to 2.6 or is 2.7 now required?
-David
On Mar 13, 2010, at 9:36 PM, Daniel Dunbar wrote:
Hi,
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 x86_64. I'd
On Sat, Mar 13, 2010 at 10:39 PM, David A. Ramos daramos at stanford.edu
wrote:
Daniel,
Are the changes backwards compatible to 2.6 or is 2.7 now required?
They are backwards compatible, KLEE should work with 2.6 and 2.7. 2.5
may even work, but I haven't tested it.
- Daniel
-David
On
Hi,
I also tried replay experiments for other test cases, and I managed to
get more details about a particular case where the replay is broken. I
found a situation where the symbolic state differs between the
original and the replay, for the same path. However, I don't know
exactly how to
Hi Stefan,
There are variations in the linking process from run to run based on Linux
address space layout randomization. I think the issue is actually on the LLVM
side. Try turning ASLR off (setarch `arch` -R klee ...) and see if that
resolves your issue.
-David
On Mar 16, 2010, at 6:53 AM,
David,
Thank you for the hint! Indeed, ASLR was the cause of discrepancies
between assembly.ll files. Now the files are perfectly identical from
one Klee run to another. Unfortunately, this doesn't solve my problem
with broken replays, so I'll have to dig deeper in the file model code
and see
Hi Cristian,
I don't believe that is the issue:
$ ulimit -a
core file size (blocks, -c) 0
data seg size (kbytes, -d) unlimited
scheduling priority (-e) 0
file size (blocks, -f) unlimited
pending signals (-i) 13335
max locked memory
On Wed, Mar 17, 2010 at 6:35 PM, Stefan Bucur stefan.bucur at epfl.ch wrote:
Hello,
When I run the Debug
version of the executable, constant arrays are not reported as being
created anymore, even though printing the symbolic state constraints
show them as being existent.
[...]
Another
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
on 03/23/2010 03:31 AM Cristian Cadar said the following:
Just ignore for now the patch for LLVM 2.7:
svn co -r 98465 http://llvm.org/svn/llvm-project/klee/trunk klee
This works, at least with llvm-2.6. (I haven't tried with the latest svn.)
Thanks.
--- Vladimir
Vladimir G. Ivanovic
$ cd /usr/local/src
$ tar xzf ../downloads/klee-uclibc-0.01.tgz
$ cd klee-uclibc
$ ./configure --with-llvm=/usr/local/src/llvm-2.6
$ make defconfig
$ make
===
./extra/scripts/conf-header.sh .config include/bits/uClibc_config.h
cc1: warning: unrecognized gcc debugging option: N
CC
Dear Daniel and Cristian,
One more thing is, if I do not declare any local var at foo() and just
return (as below), the memory usage is only about 1%.
void foo() {
return;
}
2010/3/31 Heming Cui heming at cs.columbia.edu
Dear Daniel and Cristian,
I am Heming Cui, Prof. Junfeng
Hi,
I have a few questions about computing the coverage.
I was wondering if there is a way to use run.istats to generate the
coverage just for the interesting source files (i.e., not for the
library files). If this is possible, it wouldn't be necessary to
replay the test cases and use gcov to
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
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 =
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
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
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
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
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
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...
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,
Daniel,
Thanks for the fixes and the link to a x86_64-compatible version of uClibc!
I successfully built LLVM (revision 102924) and klee (revision 102924)
using the x86_64 version of klee-uclibc
(http://www.doc.ic.ac.uk/~cristic/klee-uclibc-0.01-x64.tgz):
llvm: ./configure
Hi,
I'm trying to use klee on a subject that makes calls to the GMP and MPFR
libraries. These libraries use a lot of inline assembly, but I can
guarantee that their functions' arguments will always be concrete.
Therefore, I hoped to build GMP and MPFR as shared objects for x86_64 and
make them
Hi,
I'm trying to use klee on a subject that makes calls to the GMP and MPFR
libraries. These libraries use a lot of inline assembly, but I can
guarantee that their functions' arguments will always be concrete.
Therefore, I hoped to build GMP and MPFR as shared objects for x86_64 and
make
Hi Brady,
The -load option is indeed the right path.
The assertion you are hitting is probably something to do with an LLVM
type KLEE doesn't have support for, most likely some kind of vector
type. If you can get a small test case, please file a bug, it might
not be too hard to fix.
- Daniel
Unfortunately no. KLEE has no way to limit it's search to paths which (will
eventually) satisfy the predicates.
Ideally a very smart search strategy would handle this automatically as part of
trying to get code coverage, but it is a very hard problem.
- Daniel
On Apr 28, 2010, at 6:02,
Heinz,
Did you actually see the LLVM generated code? Perhaps a dead code
elimination optimization removed the branch and you were left with a
simple return statement. You should run llvm-dis on test.o, and check
the test.o.ll generated file, and see if that branch actually got
compiled in the
Thanks Stefan but your code doesn't work either.
$ klee test.o
KLEE: output directory = klee-out-0
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two
My apologies; I meant to reply on the mailing list, but I replied directly.
Sorry,
Brady J. Garvin
Seungbeom Kim,
I'm no expert on KLEE, but I would say from the trace that strcmp is being
evaluated by a call to native assembly. In other words, strcmp is not
compiled to LLVM bitcode, so KLEE
Very simple:
$ klee-gcc -c -g strcmp.c
$ klee strcmp.o
Oops, it seems that uclibc is not linked by default, contrary to
the older version (before open sourcing) which links it by default.
(I was confused and mistaken when I thought --posix-runtime would
enable it; it is --init-env that is
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
Hi,
I am running klee on some programs with the pread function, and klee
cannot return the correct results.
I write a test program test.c as follows.
#include stdio.h
int main(int argc, char* argv[])
{
int ch;
int input = open( tmp.txt, r );
char buf[10];
pread(input, buf, 10, 0);
printf(get
On Fri, Jan 29, 2010 at 2:07 PM, Daniel Dunbar daniel at zuster.org wrote:
Hi Liu Jian,
On Sun, Dec 27, 2009 at 6:16 PM, Liu Jian gjk.liu at gmail.com wrote:
Hi all,
I will try to apply klee to check Xen (e.x. version 3.3.0) source
code
like
your similar work to HiStar. But meet
Hi, I have a question about how klee_assume interacts with functions, in
this case the strlen function.
~/klee-test/assume_strlen:85$ cat asl.c
#include string.h
#include klee/klee.h
int main(int argc, char *argv[])
{
char resolved[8];
klee_make_symbolic(resolved, sizeof(resolved),
Hi Hemanth,
In this case you don't want the -load option, because that links native
code. Use the program llvm-ld instead. For the most part, it works like
ld; read the ld man page for more info. You can also run
$ llvm-ld --help
for the other options (there are many).
Brady J. Garvin
Hi,
I created an attachment on the bug page that seems to solve the failed
assertion problem. It would be great if you had a look and see if
there is anything wrong with the fix:
http://llvm.org/bugs/show_bug.cgi?id=6171#c5
Thanks,
Stefan
On Sat, May 15, 2010 at 6:56 PM, Daniel Dunbar
I have been trying to trace back the problems I'm having with KLEE (see
the test failures to which I referred last week) and have started to get
suspicious even of the simplest warnings.
When I run tutorial example 1 (the islower.c example) with a clean
system I get the following warnings:
$
Dear folks,
I am wondering how labels for expressions work? Could you please
tell me which part of code is handling replacing sub-expressions with
labels?
For example, given the expression below:
(Slt (Select w32 (Slt N0:(ReadLSB w32 0 n)
16)
Dear Daniel,
I did some more expressions and it seems to me that something might be
wrong with the labeling mechanism in KLEE expressions.
Once I collected two expressions and dump them to a file with KQuery
format:
-
(Eq 4294967279
Or maybe my format of storing expressions are not correct. Currently I am
storing the two expressions within one kquery file.
Maybe storing the two constraints in seperate KQuery files can solve the
problem?
2010/6/22 Heming Cui heming at cs.columbia.edu
Dear Daniel,
I did some more
Hi Heming,
Labels are global across the entire file, and are parsed in the order
they are seen in the file. So it is fine to have a definition of a
label be an inner expression.
On Tue, Jun 22, 2010 at 2:16 PM, Heming Cui heming at cs.columbia.edu wrote:
Dear Daniel,
??? I did some more
Hi Chris,
This sounds like a problem with mismatch LLVM tool versions. Most
likely you either have some existing LLVM tools on your system, or
your llvm somehow got configured with an llvm-gcc from a different
version.
I'm not sure why this is happening more commonly now, but it is almost
On Wed, May 19, 2010 at 8:23 AM, Jonathan Hohle jonhohle at gmail.com wrote:
I'm trying to build klee on 64-bit Darwin (Mac OS X) with POSIX runtime
support, but I can't get uclibc to build (its looking for asm/unistd.h, among
other things). Is it currently possible to use klee in OS X on
Hi Graham,
Sorry, it has taken me a while to take a look, but I added some
comments to the bugzilla. This is probably a mismatched LLVM tool
version of some kind, if you can give me some more information on your
build we should be able to sort it out, I added a comment asking for
the logs I would
Hi Seungbeom,
On Fri, Jun 4, 2010 at 4:10 PM, Seungbeom Kim sbkim at stanford.edu wrote:
Hi,
I find that #include iostream alone causes KLEE to segfault
at the end of the run, but not with --libc=klee or --libc=uclibc.
First, let me start by saying that trying to run KLEE on C++ code
isn't
Hi
Currently, Klee does not model network calls, therefore, instead of calling the
__socket syscall, it returns EAFNOSUPPORT.
You would need to write a network model by extending the file system model in
runtime/POSIX to be able to run network applications in KLEE. You can take a
look in
In the documentation and literature, there seems to be some confusion
about the -sym-args (or --sym-args) argument to -init-env.
klee ... -init-env ... --help
gives
-sym-args MIN MAX N - Replace by at least MIN arguments and at
most MAX arguments, each with maximum length N
The Cadar, Dunbar,
Hi Li,
klee_assume can be confusing, because it works based on the result of
the expression. In cases when the expression branched, this usually
isn't what was intended. klee_assume is roughly equivalent to:
--
void klee_assume(int constraint) {
if (!constraint) klee_silent_exit(0);
}
--
except
KLEE doesn't currently work with 'make install'. The error you are
getting is easy to fix, but KLEE still won't work because it doesn't
know how to find the runtime files once installed.
- Daniel
2010/4/17 daqi at ruc.edu.cn:
Hello. When I make install your program klee, there is an error
Hi Alvin,
KLEE does a few extra tricks when linking. In particular, uclibc
defines its own entry point so KLEE rewrites the user's main function
to be called by this entry point. I think if you just link with
llvm-ld the wrong entry point will be called, and uclibc won't end up
being initialized.
Hi Wujie,
I don't recall, to be honest, but I think KLEE doesn't currently
support pread because we use it to implement our file model, and don't
instrument it.
- Daniel
On Sun, Jun 6, 2010 at 1:15 AM, Wujie Zheng wjzheng at cse.cuhk.edu.hk wrote:
Hi,
I am running klee on some programs with
1 - 100 of 2196 matches
Mail list logo
