Dan,
Thanks for you answer. I think I've followed exactly the web site but
maybe I'm wrong. This eve I'll retry and send over here the output of the
command that you have suggested.
Thanks,
Alberto
On 25 Mar 2015 13:36, Dan Liew d...@su-root.co.uk wrote:
On 24 March 2015 at 21:16, Alberto
Hi,
Should I see the files contained in it?
I can see just not printable characters.. I followed the guide on the web
site. Any advice?
Thanks,
Alberto
On 25 Mar 2015 13:47, Alberto Barbaro barbaro.albe...@gmail.com wrote:
Dan,
Thanks for you answer. I think I've followed exactly the web site
Hi,
OK i found the solution after a break:
https://keeda.stanford.edu/pipermail/klee-dev/2012-January/000794.html
HTH,
Alberto
2015-11-07 7:49 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>:
> Hi,
> i'm trying to compiling Klee and once i run make ENABLE_OPTIMZED=1 i have
>
as an
> independent search heuristic. The bar for changing the core of KLEE is
> much higher, as it affects all users.
>
> Best,
> Cristian
>
> On 18/03/2018 17:41, Alberto Barbaro wrote:
> > Hi,
> > I'm working on a possible PULL request that would allow to execut
) call of the form:
>
> bindLocal(kinst, state, expr);
>
> you can do
>
> expr->dump();
>
> immediately after/before the call to see the expression being locally
> bound.
>
> I hope this helps.
>
> Best,
> Andrew
>
>
> On Sunday, 18 March 2018, 7:56:03 pm G
t; is much more there.
>
> Hope that helps you a bit further.
>
> Best,
> Martin
>
> On 2. May 2018, at 20:16, Alberto Barbaro <barbaro.albe...@gmail.com>
> wrote:
>
> Hi all,
> thanks for the answer. I was able to create another searcher called
> "
Hi all,
I'm working on a new searcher and I'm at a point where I would skip the
current state and just continue with the new added states. Is there a way
to do that in the updateState() function? If not, how should I do it?
Thanks a lot
___
klee-dev
Hi all,
I'm sorry to ask a question that was already asked but I cannot figure out
what I'm missing.
I'm recompiling libpng and I'm using klee_make_symbolic in the main
function as a test. The ./configure goes well but the make does not. I have
changed the Makefile and I have an error like this:
Hi all,
I would like to add a new class to KLEE but I have few problems. I tried to
follow the help that is present on the website but not luck so far.
In my case, I have created TestObject,h and TestObject.cpp in lib/Core and
included TestObject.h in lib/Core/Executor.cpp using #include
Hi,
sorry for the email... I fix it adding the file to the CMakeList.txt, I
would suggest to update the documentation on the website as well. I think
it would be useful to everybody.
Thanks
2018-03-10 6:17 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>:
> Hi all,
> I would
on. Just open
> a pull request at https://github.com/klee/klee.github.io
>
> Best,
> Cristian
>
> On 10/03/2018 07:08, Alberto Barbaro wrote:
>
>> Hi,
>> sorry for the email... I fix it adding the file to the CMakeList.txt, I
>> would suggest to update t
Hi all,
I have seen that the malloc function is handled via handleMallc() in
Executor.cpp relying on executeAlloc(). I would like to understand the best
way to access, for instance, to address associated with the memory
allocated by the malloc. I think the function bindLocal() is used for
storing
Hi,
I'm working on a possible PULL request that would allow to execute a
project but excluding paths based on a .path previously generated using
KLEE. Doing so it would be possible to have some sort of "exploration
technique" that would help to follow specific paths.
I think, after having
and if is
encountered 2 states are returned, the first should be the false branch
instead the second should be the true branch. Am I right? At this point
should I terminate the other state?
Thanks for your time.
A
2018-03-18 20:43 GMT+00:00 Alberto Barbaro <barbaro.albe...@gmail.com>:
> Thanks I'
ndent search heuristic. The bar for changing the core of KLEE is
> much higher, as it affects all users.
>
> Best,
> Cristian
>
> On 18/03/2018 17:41, Alberto Barbaro wrote:
> > Hi,
> > I'm working on a possible PULL request that would allow to execute a
> > project
Thanks Dan,
all clear now.
Thanks again
2018-03-03 21:23 GMT+00:00 Dan Liew <d...@su-root.co.uk>:
> Hi,
>
> On 3 March 2018 at 07:29, Alberto Barbaro <barbaro.albe...@gmail.com>
> wrote:
> > Hi all,
> > few months ago I was trying to understand how to test p
-03-03 21:10 GMT+00:00 Cristian Cadar <c.ca...@imperial.ac.uk>:
> Hi, there in an open PR about this, which you might like to use, although
> it still requires some work: https://github.com/klee/klee/pull/473
>
> Best,
> Cristian
>
>
> On 03/03/2018 08:06, Alberto Barb
Hi all,
few months ago I was trying to understand how to test pngpixel via KLEE and
after few suggestion I was able to do it.
I have just one more question. When I run KLEE I have this output:
klee@0c7da896b087:~/targets/libpng-1.6.34/contrib/examples$ klee
--libc=uclibc --posix-runtime
Hi all,
I have already asked this in the past and received few suggestions but I
was not able to do it. I'm trying to test pngpixel[1] that takes as input
an image file. My goal is to execute pngpixel with a real file and
subsequently execute pngpixel with a symbolic file and follow the path
puts, then use the ktest file as a seed. In this way,
> all inputs will be symbolic, yet the path is the one that would have been
> executed using the concrete inputs.
>
> Best,
> Andrew
>
> On Sun, Oct 14, 2018 at 8:25 PM, Alberto Barbaro
> wrote:
> Hi all,
>
te) seeds, and when there is only one seed, it
> is somewhat similar to concolic execution. But you need to:
> + tell KLEE that you only want to run seed (-only-seed) and you only want
> to replay seeds (-only-replay-seeds), and
> + re-start KLEE for each run of each seed.
>
> Cheers
expect output should be:
klee@a8a6399e6799:~/seeds$
../target/libpng-1.6.35/contrib/examples/pngpixel 1 1
../images/png-files-download.png
RGBA 255 255 255 255
klee@a8a6399e6799:~/seeds$
What am I missing? :)
Thanks for your help!
Alberto
Il giorno mar 16 ott 2018 alle ore 14:27 Alberto Barbaro
which case only one path is
> traversed.
>
> Best,
> Andrew
>
> Sent from Yahoo Mail on Android
> <https://go.onelink.me/107872968?pid=InProduct=Global_Internal_YGrowth_AndroidEmailSig__AndroidUsers_wl=ym_sub1=Internal_sub2=Global_YGrowth_sub3=EmailSignature>
>
> On Sat
Thanks I'll try that one later :)
On Tue, Oct 16, 2018, 14:08 Sang Phan wrote:
> You need to pass -allow-seed-extension (or -allow-seed-truncation) when
> the seed is shorter (or longer) than the symbolic file
>
> On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro <
> barbaro
Hi all,
I'm on a searcher and I would like to remove the current state from states.
Should I added it to removedStates or do something else? Can I have the
example one line code if not too much?
Thanks
___
klee-dev mailing list
klee-dev@imperial.ac.uk
Hi all,
I was able to compile httpd but unfortunately I cannot really execute it
because the sockets are not really supported. I've seen that also someone
else had the same problem a while ago. In my opinion, this is an important
issue because sockets are everywhere... What's your view on that?
wrote:
> Hi Alberto,
>
>
> On Fri, 26 Oct 2018 13:41:45 +0100
> Alberto Barbaro wrote:
>
> > I'm on a searcher and I would like to remove the current state from
> states.
> > Should I added it to removedStates or do something else? Can I have the
> >
Thanks Frank,
ASAP I'll try to use the approach you suggest and if working fine I could
submit a PR if for you is OK.
Thanks
Il giorno lun 29 ott 2018 alle ore 16:00 Frank Busse <
f.buss...@imperial.ac.uk> ha scritto:
> Hi Alberto,
>
>
> On Mon, 29 Oct 2018 14:21:28 +
(ZExt w32 (Read w8 57 A-data
> N0
> 4294967295) to value 541597261
> (/home/klee/target/libpng-1.6.35/png.c:3371)
>
> Best,
> Andrew
> On Saturday, 20 October 2018, 1:51:56 AM GMT+8, Alberto Barbaro <
> barbaro.albe...@gmail.com> wrot
Hi all,
I'm generating the .smt2 file for the following simple c program:
#include
int main() {
int a;
int another;
klee_make_symbolic(, sizeof(a), "a");
klee_make_symbolic(, sizeof(another), "another");
if ( a == 77 ) {
a += 6;
another = 5;
} else {
a = 9;
if ( another == 12 ) {
a += 7;
}
be 9 (or any other value) athe end of ktest3.
Thanks
On Sat, Nov 10, 2018, 20:29 Frank Busse Hi,
>
>
> On Sat, 10 Nov 2018 07:07:13 +
> Alberto Barbaro wrote:
>
> > I feel I'm missing something because, for instance, I cannot see the
> > case where a = 0 and anoth
Hi Yuanfei,
Please have a look at the end of
https://klee.github.io/tutorials/testing-function/ , it should describe
what you need.
Thanks
On Tue, Nov 13, 2018, 22:52 Yuanfei Bi Hi, all,
>
> I run klee and got following result from ktest-tool:
>
> object1: name: b'arg0'
> object1: size:
32 matches
Mail list logo
