Hi Felicia,
Please correct me if I’m wrong: my understanding of your question is that we
first added a constraint
(x <= 0) and then changed x so you were not sure if the constraint still holds
- is that correct?
If that is the question, then I believe KLEE should already handle the
situation
be replace before solving.
or how to do it ?
thanks
xqx
2015-05-20 22:58 GMT+08:00 Kuchta, Tomasz t.kucht...@imperial.ac.uk:
Hi,
When you say failed, do you mean that the branch was not feasible?
If that is the case, it means that there are no such values in the program
not familiar with seed mode in KLEE. As far as I know, ZESTI
functionality is not available in the mainline KLEE.
Thanks again.
xqx
Best regards,
Tomek
2015-05-21 23:12 GMT+08:00 Kuchta, Tomasz t.kucht...@imperial.ac.uk:
Hi,
Thanks for the additional information.
You are right
Hi,
When you say failed, do you mean that the branch was not feasible?
If that is the case, it means that there are no such values in the program
input that would make the program execute certain path.
Or do you want to just replace symbolic data with concrete values?
If that is the case, one
Hi Tom,
On 19 May 2015, at 03:10, Tom Ritter t...@ritter.vg wrote:
On 18 May 2015 at 05:03, Kuchta, Tomasz t.kucht...@imperial.ac.uk wrote:
Hi Tom,
You mentioned that you compile llvm 2.9 from source using clang 2.9.
Did you try also with llvm-gcc? I think that if you go for 2.9
Hi Tom,
You mentioned that you compile llvm 2.9 from source using clang 2.9.
Did you try also with llvm-gcc? I think that if you go for 2.9, that probably
needs to be llvm-gcc as well.
Best regards,
Tomek
On 16 May 2015, at 05:24, Tom Ritter t...@ritter.vg wrote:
Hi all,
I think this
Hi,
On 25 Mar 2015, at 20:52, Anitha B Gollamudi anitha.boyap...@gmail.com
wrote:
On 25 March 2015 at 16:51, Anitha B Gollamudi anitha.boyap...@gmail.com
wrote:
Hi,
I would like to use KLEE for string analysis (for analyzing SQL
injection vulnerabilities). Here are my concerns:
1.
You may want to check if you have stack limit set to unlimited (you can do this
using ulimit -s).
Best regards,
Tomek
On 27 Feb 2015, at 10:52, Cristian Cadar c.ca...@imperial.ac.uk wrote:
I cannot reproduce this on my machine. Can you open an issue at
Hello,
The KLEE binary should be in: klee directory/Release+Asserts/bin/
In order for shell to see the binary, you can, e.g., add this directory to your
PATH variable.
Best regards,
Tomek
On 2 Dec 2014, at 03:52, Wei Wen wei.w...@gmail.com wrote:
Hello,
I successfully built KLEE.
Hi Mark,
I’m not sure if I understood the question correctly. My understanding was that
you would like to define a safe region for the application and then treat all
the memory accesses falling outside of that region as invalid - is that correct?
One idea might be to do that with an additional
the solution to be as push-button as possible, but I'd like to hear a
bit more about your proposal.
Thanks,
Mark
On Sat, Nov 22, 2014 at 6:48 AM, Kuchta, Tomasz t.kucht...@imperial.ac.uk
wrote:
Hi Mark,
I’m not sure if I understood the question correctly. My understanding was
that you
that takes some time
to do similar computations each time. That being said, compiling with
-O1 helps.
Sylvain
HTH,
Best regards,
Tomek
On Fri, Sep 12, 2014 at 07:11:38AM +, Kuchta, Tomasz wrote:
Hi Sylvain,
Regarding your question from the first e-mail - as far as I know
Hello,
The officially supported operating system for KLEE is Linux, I’m afraid you
will not be able to run it on Windows.
Best regards,
Tomek
From: Dinh Ngoc Thi dinhngoc...@gmail.commailto:dinhngoc...@gmail.com
Date: Wednesday, 1 October 2014 15:14
To: klee-dev
Hi Sylvain,
Regarding your question from the first e-mail - as far as I know there is
no easy way to get all possible values, except
for adding inequalities to the set of constraints, but if there exists one
I would be happy to learn about that.
One possible issue related to this problem is when
,
because the pointer that we create using the constrained symbolic value ‘x’ can
be pointing at three different memory
objects.
Hope that helps.
Tomek
From: Sandeep sdasg...@illinois.edumailto:sdasg...@illinois.edu
Date: Wednesday, 8 January 2014 16:58
To: Kuchta, Tomasz
t.kucht
Hello,
You could try to do the following to print the name of the symbolic variable:
In lib/Core/SpecialFunctionHanlder.cpp there is a handler named
handleMakeSymbolic.
At the beginning of the handler, there is an if-else block and in the ‘else’
part
‘name’ string is set.
You could try to add
Hi Bowen,
The way to do that is the following:
- at the beginning of the file you will find a list of arrays
- from the list, you choose the name of the array that you are interested in
- .pc file probably ends with false)
- the way to get the value of the selected array is to modify
Hello,
I came across the following script:
https://github.com/travitch/whole-program-llvm
Unfortunately, I am unable to tell whether it will work for openssl or texinfo.
I thought that maybe it will be useful for you.
Best regards,
Tomek Kuchta
On 15 Aug 2013, at 14:56, l...@seg.nju.edu.cn
I've just noticed the same. I would try to do make clean, configure once more
and then as Jonathan's said.
Thanks,
Tomek
On 17 May 2013, at 10:15, Jonathan Neuschäfer j.neuschae...@gmx.net wrote:
On Fri, May 17, 2013 at 12:51:26PM +0800, wnta wrote:
Dear All:
I use ubuntu 12.04,and
Hello,
I know that it runs under Linux and also heard about MacOs (however I do not
know current status) and they are both Unix based.
I am not sure - maybe someone on the list will know.
Best Regards,
Tomek
On 25 Apr 2013, at 06:38, ?? 1196467...@qq.comhttp://qq.com wrote:
can you tell
Hello,
Please also try setting
export LIBRARY_PATH=/usr/lib/x86_64-linux-gnu
Best Regards,
Tomek
On 22 Apr 2013, at 04:32, Loi Luu
loi.luu...@gmail.commailto:loi.luu...@gmail.com wrote:
Dear all,
I got the same error in this thread
From: Daniel Schwartz-Narbonne [d...@cs.nyu.edu]
Sent: 08 April 2013 17:52
To: Kuchta, Tomasz
Cc: klee-dev
Subject: Re: [klee-dev] Problem Installing KLEE
I switched to the 64 bit version of llvm-gcc, but that didn't fix it
Daniel
On Fri, Apr 5, 2013 at 5:53 AM, Tomasz Kuchta
22 matches
Mail list logo
