[klee-dev] How Klee processes loop

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev