Hi Adarsh,
During the actual symbolic execution, KLEE does not use any information
about loops. However, you can recover this info from the LLVM module,
on which KLEE operates. LLVM is well documented, please see here:
https://llvm.org/docs/
Best wishes,
Cristian
On 08/06/2024 18:16, Adarsh Sudheer wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
