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

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



When some proofs fail on really simple properties that are in fact trivial, it often means that the generated goal does not have the right form for SMT solvers. 
In such a situation, one wants to provide either another goal that have the same sense, but is easier to handle, or to provide some lemmas to solvers so that they can deal with it. 

There are several ways to add simplifiers to WP. 

The most basic one is simply to write axioms or lemmas in ACSL, these lemmas can then be used by SMT solvers. 

A more integrated way to do this, is to write a WP driver bound to a Why3 theory: 

1. Write a Why3 theory where the necessary types, symbols and their properties are stated 
2. Prove the necessary lemmas in Why3, perhaps using Coq on the most tricky parts 
3. Use a WP driver to bind your Why3 theory to abstract ACSL symbols, that you can now use within your code annotations. 

I think that the WP manual talks about it. 

Finally, it is possible to add simplifiers to the Qed module so that they can be used during simplification phase. 
It is extremely efficient, but also complex to write, and a mistake can make any proof unsound as it must be done by writing new Ocaml code in Qed. 

Best, 
Allan B. 


De: "Quentin Santos" <qsantos at qsantos.fr> 
À: "Frama-c-discuss" <frama-c-discuss at lists.gforge.inria.fr> 
Envoyé: Mardi 22 Septembre 2020 10:53:24 
Objet: Re: [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 | 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 | https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-November/005180.html ] 
Best regards,
Quentin Santos 

_______________________________________________ 
Frama-c-discuss mailing list 
Frama-c-discuss at lists.gforge.inria.fr 
https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200922/d372de4e/attachment.html>