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] Tim's question about unusually fast analysis involving Frama_C_interval(0, 0xffffffff)

  • Subject: [Frama-c-discuss] Tim's question about unusually fast analysis involving Frama_C_interval(0, 0xffffffff)
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 6 Aug 2015 17:04:21 +0200
On the why3-club mailing-list (
https://lists.gforge.inria.fr/pipermail/why3-club/2015-August/001273.html
), Tim Newsham asked:

\\\
I came up
with the less creative approach of

    n = Frama_C_interval(0, 0xffffffff); // in caller

    while(n--) update(...); // in the hash model function

and surprisingly when I run this through frama-c it seems
to analyze fairly quickly (compared to the other solution)
and not give any warnings.  My question here is -- why?
This makes me think that perhaps there is a hidden error
here.
///

The approach of using n = Frama_C_interval(0, <some large number>); and
while(n--) …;
is fine in principle. The property being proved is slightly less general,
but for say, 0x7fffffff, the number of iterations that would be necessary
to unroll the loop completely is so large that it's a good bet that the
value analysis does not obtain its result by unrolling the loop but by
finding a fixpoint for it. Which is abstract interpretation talk for
“automatically find some sort of weak inductive invariant for the loop”.
And can be expected to basically take the same time than the while
(Frama_C_interval(0, 1)) driver.

However, for the particular argument 0xffffffff, one problem is that
Frama_C_interval is defined by the prototype and contract:

/*@ requires min <= max;

    assigns \result \from min, max, Frama_C_entropy_source;

    assigns Frama_C_entropy_source \from Frama_C_entropy_source;

    ensures min <= \result <= max ;

 */

char Frama_C_char_interval(char min, char max);


The prototype causes the function to be actually applied to 0 and -1. The
contract tells the value analysis that it can be assumed by transitivity
that 0 <= -1 each time the function terminates.


When we realized this limitation of the Frama_C_interval function, we added
more functions including a Frama_C_long_long_interval one that would have
been appropriate to handle the large values here. These functions are all
in a file named __fc_builtin.h.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150806/54a880e9/attachment.html>