Hi Mathew,
I cannot reproduce this on my machine with the latest KLEE and LLVM 16.
Can you make sure you are running the latest version of the codebase, as
the file and line number that you reference suggests otherwise. If so,
how exactly are you running KLEE on this example?
Best wishes,
Cristian
On 21/08/2026 09:26, Mathew via klee-dev wrote:
Hi together,
I ran into a hard crash of the whole KLEE process when running a simple
program that contains a variable-length array whose size is symbolic.
Setup: LLVM 16, KLEE built from source with uClibc and POSIX runtime, on
Ubuntu.
Test program:
#include <klee/klee.h>
int main() {
unsigned x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume(x >= 1);
klee_assume(x <= 20);
int buffer[x];
buffer[0] = 1;
return buffer[0];
}
Running this code snippet aborts the entire process with the following
error:
LLVM ERROR: Cannot lower a call to a non-intrinsic function
'llvm.stacksave.p0'!
...
klee::IntrinsicCleanerPass::runOnBasicBlock(...) IntrinsicCleaner.cpp:425
...
Aborted (core dumped)
I found issue #1754 on GitHub, which lists llvm.stacksave among the
"unimplemented intrinsic" warnings after upgrading to LLVM 17. So my
case with LLVM 16 seems to have a different reason.
My question: is a full process abort the intended behavior for
variable-length arrays with a symbolic size, is this specific to my
setup, or is this a bug?
Thanks in advance
Mathew
_______________________________________________
klee-dev mailing list -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
klee-dev mailing list -- [email protected]
To unsubscribe send an email to [email protected]
