Hi Daniel,
Thanks a lot for your suggestion. I've tried it and it solved the issue.
However, it moved it down to the solvers. Now it is STP and Z3 who get
their stacks blown up. See the backtrace here:
https://pastebin.com/raw/WE2M0bJf
I also set `ulimit -s unlimited` and now they all seem to be
Hi Marco,
I had a look at your stack trace, and the crash might have been caused
by KLEE when building the solver query before passing it to the actual
solver. Could you check out https://github.com/klee/klee/pull/1523 and
see if that changes anything for you?
Best,
Daniel
On 2022-06-18
ine that I am interpreting is extremely
simple.
Best,
Marco
> Best,
> Manuel.
> --
> *From:* klee-dev-boun...@imperial.ac.uk
> on behalf of Cristian Cadar
> *Sent:* 17 June 2022 10:53
> *To:* mvano...@dc.uba.ar ; Nowack, Martin <
> m.now
Hi Cristian,
Thanks for your answer. I have tried *--optimize-array=all*, but that
didn't fix the problem :(.
It would be a better user experience to get an error message instead of a
segfault. In any case, if this is stopping because it's running out of
memory, is there a way to remove that
: klee-dev
Subject: Re: [klee-dev] Working with fixed memory locations.
Hi Marco, you seem to be reaching an issue with the solver, which is
having trouble reasoning about the huge symbolic array (requiring
excessive time and memory). You should try to shrink that array if
possible. You can also try
Hi Marco, you seem to be reaching an issue with the solver, which is
having trouble reasoning about the huge symbolic array (requiring
excessive time and memory). You should try to shrink that array if
possible. You can also try --optimize-array=all, but it might not help
in your case.
After letting it run for a few hours I've observed that klee spawns a
subprocess that keeps growing on memory until it reaches ~100GiB and then
it stops and restarts again.
Nothing is being printed indicating an error, but I'm not sure if the
behavior is normal. This is with KLEE from the docker
Hi Martin, Manuel,
Thanks for your answer :) !
On Thu, Jun 16, 2022 at 1:19 PM Nowack, Martin
wrote:
> Hi Marco,
>
> Maybe the following helps you:
>
> https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c
>
This seems to be what I am
Hi Marco,
Maybe the following helps you:
https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c
Best,
Martin
On 16. Jun 2022, at 20:43, Carrasco, Manuel G
mailto:m.carra...@imperial.ac.uk>> wrote:
Hi Marco!
I have a program that when
Hi Marco!
I have a program that when compiled, adds a program header that loads a data
blob into a fixed memory location.
I'm sorry to ask, but could you explain a bit more how this works? At first
glance, I'd say that if any of this happens on a stage later than LLVM-IR, it
may be hard to
10 matches
Mail list logo
