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