# 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] hint assertions and understanding cooperation between wp and value plugin

*Subject*: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin*From*: boris at yakobowski.org (Boris Yakobowski)*Date*: Sun, 1 May 2016 22:24:40 +0200*In-reply-to*: <87fuu82u9r.fsf@inria.fr>*References*: <87fuu82u9r.fsf@inria.fr>

Hi again, Regarding WP, as you understood, the Real model is unsound for your lemma /*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */ You will have to use the Float model for such a proof. And then the proof will fail (hopefully!), since this property is false. > is verifiable and value analysis shows that x*x >= 0 > with -val-subdivide-non-linear 1094 This setting (1094) seems a bit high for such a simple formula. Out of curiosity, what were the possible values for x? > On the other side, (x - .1)*(x - .1) >= 0 is verifiable with -wp > -wp-model float but I did not manage to verify it with the value plugin > alone and -val-subdivide-non-linear (I stopped the computation after > 99999) Again, this is a bit strange. I'm able to analyse the following program and prove that r >= -0. using -val-subdivide-non-linear 1080. You may obtain different results with different bounds for x, because the subdivision strategy depends on the initial interval. However, there should be no need to go to extreme values such as 99999. void main(double x) { double r = (x - .1)*(x - .1); } Regarding x*x - .2 * x + 0.01 >= 0., I tried to see if I could *dis*prove it using Value, and then find the best possible bound, using -val-subdivide-non-linear for both. These are the results of my investigation: 1. the current algorithm is unsuitable for very high arguments (say > 10.000). From an algorithmic standpoint, the list of intervals that remain to be considered should be replaced by a heap. We will improve this for Frama-C Silicium. All my experiments were carried out with such a heap 2. the detection that no further improvement can be made to the final result could also be improved. For example consider: void main(float x) { float r = x * x - 0.2 * x + 0.01; } I believe that the tightest lower bound for r is -0x1.70a3d8p-32. The current version of -val-subdivide-non-linear fails to notice that this value must be in the result and keeps subdividing intervals -- even though their image is included in [ -0x1.70a3d8p-32 .. \infty]. This is inefficient, as bigger arguments to -val-subdivide-non-linear will result in longer analysis times without any final gain in precision. 3. Value and -val-subdivide-non-linear find values that refute x*x - .2 * x + 0.01 >= 0. ; for example r = -0x1.0p-59, obtained for x = 0x1.9999998p-4 after 43626 subdivisions. However, this information is not available to the user. This is due to the fact that -val-subdivide-non-linear is not goal-directed. Also, Value is designed to over-approximate, while we need an *under*-approximation in this case. 4. finding the tightest possible bound using variables of double type is out-of-reach with this approach. The best results I obtained, after 2.500.000 subdivisions and around 1h30 of computation, were r >= -0x1.3ad1000000000p-43 -- while I suspect the maximally negative value is -0x1.0000000000000p-59. After 1.000.000 subdivisions (38 minutes), the best bound is -0x1.994bffffff08dp-41. So the convergence is slow. This is to be expected given the algorithm and the search space. 5. on the other hand, with variables of float type, an exhaustive search is possible (and fast!) on this example: less than 3s. This is how I derived the bound for point 2. This unfortunately does not generalize to expressions such as x * x - 0.2 * x + 0.01 - (x-0.1)*(x-0.1) in which the numeric "noise" is prominent, though. In any case, thanks for this very interesting example! -- Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160501/3993e186/attachment.html>

**Follow-Ups**:**[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin***From:*Maurice.Bremond at inria.fr (Maurice Bremond)