Hi all
I met a problem which loop cause path explosion.
For example, there are 3 variables, control_block, p_data and event.
Control_block and p_data are structures and have some fields as symbolic. Event
is an integer between 0 to 42.
Now I want to run smp_sm_event(control_block, p_data, event) for each event.
When manually set event from 0 to 42 (which means, runs klee for 42 times),
klee can get result quickly with each case finishing in controllable
instruction number.
However, when I try to run the following:
for (int event=0; event<=42; event++) {
smp_sm_event(control_block, p_data, event)
}
Then klee's running seems never ends. When manually halt klee, it finishes with
more than 10 million instructions.
May I get some advice on why this happen, and is there way to solve this
problem so that I don't need to manually run klee for many times? Thank you!
--------------------
Best regards,
Weixuan
Master student in Computer Science, Penn State University
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
