--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2020 ---
Thanks for the quick reply Allan, I had somehow completely missed the fact that WP included an interactive proof editor! I figured this tab was only meant to inspect goals and try to understand why a proof failed. Thanks a lot for pointing that out. It does allow me to prove such goals without changing the code. In passing, when I say âbugâ, I do mean âunexpected behavior for the userâ, not that it is unsound of course. You allude to the fact that this could be fixed by adding a simplifier. Is there a document I could start with to get myself acquainted better with the inner workings of Frama-C and WP to improve my intuition on this kind of behaviors, besides jumping right into the source? For anyone reading this and who wouldn't already know this, I want to add that âshouldn't the right-hand side expression already be of type int?â in my previous mail actually does not make sense, since ACSL deals with real values, so the cast to int is actually needed, although it should be trivially proved. I realized this by reading [1]. Also, my initial surprise was due to the fact that the C spec actually gives an arithmetic definition of the bitwise shift, but WP seems to only consider the logical meaning [2]. [1] https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2015-October/004970.html [2] https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-November/005180.html Best regards, Quentin Santos -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200922/16e7b67e/attachment.html>