[klee-dev] How to solve path explosion caused by loop?

[Wang, Weixuan]

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

-------------- next part --------------
HTML attachment scrubbed and removed