CAUTION: This message came from outside Imperial. Do not click links or open
attachments unless you recognise the sender and were expecting this email.
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]
