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 Sandip,
Those constants are most likely derived from concrete addresses, but you
should try to simplify the program as much as possible and send a full
program that can be compiled and run.
Best,
Cristian
On 02/05/2022 19:22, Sandip Ghosal wrote:
Hello,
I need help in understanding a
Hi Yukai,
You can use klee_assume
(https://klee.github.io/docs/intrinsics/#klee_assumecondition) on the
desired symbolic file created by the POSIX runtime, see
https://github.com/klee/klee/blob/master/runtime/POSIX/fd_init.c#L61
Best,
Cristian
On 06/06/2022 15:06, 房合钧 wrote:
Hello!
I
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
You should look at the work of Alastair Reid / Google on this topic:
https://project-oak.github.io/rust-verification-tools/2021/07/14/coreutils.html
Best,
Cristian
On 04/06/2022 22:26, gwpub...@wp.pl wrote:
Klee got famous with coreutils experiments.
As they reimplement coreutils in Rust,
Hi,
On Mon, 2 May 2022 09:50:23 +0200
Niklaus Leuenberger wrote:
> For this I have written following KLEE harness:
> ---
> #include "klee/klee.h"
> #include "buggy_api.h"
> int main(void) {
> for (int i = 0; i < 2; ++i) { // sequentially call 2 APIs
> int f_select = klee_choose(2);
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
Hi Niklaus,
There is no obvious improvement to recommend for the general case. Of
course, search heuristics have an important influence on which API
sequences are explored first. There is also a lot of research into this
problem: I would recommend Randoop
Hi Austin,
Sorry to see that nobody has answered your email. I'm not sure what you
are trying to do though. Are you trying to make KLEE choose a specific
size?
(That code is a bit broken, btw. We fixed it in some extensions but
haven't managed to merge the changes into the mainline yet.)
Hi klee-dev!
I am new to KLEE, and have a question about using it with one of my
programs.
I have a program that when compiled, adds a program header that loads a
data blob into a fixed memory location.
This means that my program has this fixed memory location hardcoded all
around the place
11 matches
Mail list logo
