Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>