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>