[klee-dev] KLEE Path Exploration Issue with -O1/-O2 Optimization Flags

[Cristian Cadar]

Hi,

Such behaviour may occur due to compiler optimisations.  You can take a 
look in klee-last/assembly.ll to see the LLVM bitcode executed by KLEE.

Best,
Cristian

On 27/10/2024 13:21, Sun wrote:
> Dear KLEE Community,
> I’m facing an issue in KLEE when compiling with -O1 or -O2optimization 
> flags. Using -O0, KLEE generates 16 test cases as expected, but with 
>   -O1 or -O2, it only generates one, despite klee_assume settings meant 
> to guide path exploration.
> Is this limited path coverage expected due to optimizations, or are 
> there settings to preserve full path exploration at higher optimization 
> levels?
> Thank you for any insights!
> Best regards
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev