--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on September 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP-RTE on simple bitwise shift operation



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>