--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] math vs. bits



Hello,

On Tue, Nov 12, 2013 at 1:17 AM, Claude Marche <Claude.Marche at inria.fr>wrote:

>
> I'm not sure Jessie is the right tool for that, The Value plugin or the
> WP plugin might do better.
>

The value analysis plug-in is not designed to verify properties expressed
as equations between argument and result, such as:

ensures x <= INT32_MAX ==> \result == 2 * x ;

At the time John posted about saturating arithmetic functions that he gave
to implement in standard C to his students (
http://blog.regehr.org/archives/277 ,
http://blog.regehr.org/archives/392), I tried to verify my own
solutions (correct ones, obviously) in Frama-C.
Not much was missing in order to be able to do the exercise in Jessie.

This time, what the value analysis plug-in was missing was the ability to
hold relational information between the two inputs. The documentation
recommends case analysis for this situation. The value analysis plug-in
typically required the O(n^2) input space (with n the number of values each
of the arguments could take) to be sub-divided by hand into O(n) cases for
separate analysis. That was tedious for 32-bit integer inputs and
impossible for 64-bit integer inputs.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/98ed50a8/attachment.html>