[klee-dev] How Klee processes loop

[Adarsh Sudheer]

Hi all,

I was wondering if there is any way klee stores the loop information. I
tried to find something useful in the opcodes of Kinstruction but it
consisted of only Br (braching) and Cmp statements. I realized that the
bitcode  implementation of loops were a combination of these statements
with exit. So I would like to know the specific characteristics that the
execution state encounters when the program counter hits the while loop and
how can one differentiate from a simple if clause.

WIth Regards
Adarsh Sudheer
-------------- next part --------------
HTML attachment scrubbed and removed