Thanks a lot.
I am going to move forward taking into account your suggestions.
Kind regards,
Manuel
On 2/6/21 21:39, Nowack, Martin wrote:
> Hi Manuel, hi Alastair,
>
> Currently, KLEE runs still the `CFGSimplificationPass` even with
> `—optimize` off.
>
I think a KLEE dev will need to suggest how to prevent the optimization
from happening.
KLEE has a flag controlling optimization "--optimize" - but it is supposed
to be off by default
--
Alastair
On Wed, Jun 2, 2021 at 4:49 PM Manuel Carrasco
wrote:
> Thanks for your answer!
>
> You hit the
Hi Manuel, hi Alastair,
Currently, KLEE runs still the `CFGSimplificationPass` even with `—optimize`
off.
https://github.com/klee/klee/blob/24badb5bf17ff586dc3f1856901f27210713b2ac/lib/Module/KModule.cpp#L288
This might be not necessary anymore for recent LLVM versions.
The best way forward
Thanks for your answer!
You hit the nail on the head. The /assembly.ll /file contains:
| %original_result = call i1 @original(i32 %a_value, i32 %b_value)||
|| %final_result = call i1 @final(i32 %a_value, i32 %b_value)||
|| %equal = icmp eq i1 %original_result, %final_result||
|| %spec.select
