forked from davidtr1037/chopper
-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
InterleavedSearcher: choose() called on empty tree during recovery #23
Comments
This is related to main.c: #include <klee/klee.h>
int global;
int a3;
void f3r()
{
global = a3;
}
void f3w()
{
a3 = 1;
}
int main(int argc, char *argv[]) {
f3w(); // skip this
f3r();
return global;
}
kleegacy -libc=uclibc --skip-functions=f3w main.bc
KLEE: NOTE: Using klee-uclibc : /home/ubuntu/code/chopper/legacy_build/Release+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/home/ubuntu/code/chopper/examples/exrecovery/klee-out-9"
Using STP solver backend
KLEE: Runnining pointer analysis...
KLEE: Runnining reachability analysis...
KLEE: Runnining mod-ref analysis...
KLEE: WARNING: undefined reference to function: __crit_2_0
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 94718872635568)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
INFO: Points-to analysis took 0 sec 0 ms
INFO: Reaching defs analysis took 0 sec 0 ms
INFO: Adding Def-Use edges took 0 sec 0 ms
INFO: Computing control dependencies took 0 sec 0 ms
INFO: Finding dependent nodes took 0 sec 0 ms
INFO: Slicing dependence graph took 0 sec 0 ms
INFO: Sliced away 1 from 4 nodes in DG
INFO: saving sliced module to: test.sliced
KLEE: done: total instructions = 3460
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
KLEE: done: recovery states = 1
KLEE: done: generated slices = 1
KLEE: done: created snapshots = 1 |
Fixed by klee/klee#1207 |
jordr
changed the title
choose() called on empty tree during recovery
InterleavedSearcher: choose() called on empty tree during recovery
Mar 2, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
~~TODO: try to reproduce with legacy Chopper ~~
E: this is a KLEE bug
The text was updated successfully, but these errors were encountered: