# 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*: loic.correnson at cea.fr (Loïc Correnson)*Date*: Thu, 21 Apr 2016 17:18:23 +0200*In-reply-to*: <87k2jrkp3q.fsf@inria.fr>*References*: <87k2jrkp3q.fsf@inria.fr>

The reason for the needed cooperation of WP and Value on this example is quite simple : - WP fails into proving that the sum of squares is finite, while Value succeed provided they are positive - WP succeed into proving that a square is positive, while Value fails because of a `-0.0` lower bound (see the GUI) Inserting the assertions make the separation of concerns explicit, and each plug-in works separately, recovering knowledge from each others. Hence, combining the two, you succeed. However, one may argue that there is surely something wrong with the `-0.0` lower bound. Notice also that the default model for WP on float is to compute over reals, without any rounding... Another way to ease the cooperation is to spread the properties over multiple ensures and requires : /*@ requires \is_finite(x) ; requires x >= 0.; assigns \nothing; ensures \is_finite(\result); ensures 0. <= \result <= 1 + x; */ extern double sqrt(double x); /*@ requires -1.0e+6 <= x <= 1.0e+6; requires -1.0e+6 <= y <= 1.0e+6; assigns result[0]; ensures \is_finite(result[0]); */ void f(double x, double y, double *result) { *result = sqrt(x*x+y*y); } This, way, you donâ€™t need intermediate assertion at all. Using the GUI, you can inspect which property has been proven by each plug-in. L. > Le 21 avr. 2016 Ã 16:34, Maurice Bremond <Maurice.Bremond at inria.fr> a Ã©crit : > > > Hello, > > Considering C implementations of some real-valued functions, I would > like to have an automated proof that, for some correctly bounded > numerical inputs within the function domain, only finite results are > returned. > > Here is a simple example with the implementation of the 2D Euclidian > norm below: > > void f(double x, double y, double *result) > { > *result = sqrt(x*x+y*y); > } > > Being interested only on the [-1e6, 1e6]^2 domain and guessing that, on > this domain, the computation should not overflow, my first attempt is to > write: > > #include <__fc_builtin.h> > /*@ > requires \is_finite(x) && x >= 0.; > assigns \nothing; > ensures \is_finite(\result) && 0. <= \result <= 1 + x; > */ > extern double sqrt(double x); > > > /*@ requires -1.0e+6 <= x <= 1.0e+6; > requires -1.0e+6 <= y <= 1.0e+6; > assigns result[0]; > ensures \is_finite(result[0]); */ > void f(double x, double y, double *result) > { > *result = sqrt(x*x+y*y); > } > > int main() > { > double x = Frama_C_double_interval(-1.0e+6, 1.0e+6); > double y = Frama_C_double_interval(-1.0e+6, 1.0e+6); > double result[1]; > f(x, y, result); > } > > > I run frama-c (Magnesium + alt-ergo 1.01) like this: > > frama-c -val t.c -wp -wp-alt-ergo-opt="-backward-compat" -then -report > > Unfortunately, the precondition on sqrt, x*x + y*y >= 0, cannot be > verified. Trying with other solvers (z3, cvc4, cvc3, zenon) and > incrementing the timeout does not help. > > With the insertion of intermediate assertions, as hints, the wp plugin > alone is not able to validate the sqrt precondition but is able to > validate the assertions, the value plugin cannot validate the inserted > assertions but, with the results of the wp plugin, is able to validate > the sqrt precondition. > > /*@ requires -1.0e+6 <= x <= 1.0e+6; > requires -1.0e+6 <= y <= 1.0e+6; > assigns result[0]; > ensures \is_finite(result[0]); */ > void f(double x, double y, double *result) > { > double x1 = x*x; > /*@ assert x1 >= 0; */ > > double x2 = y*y; > /*@ assert x2 >= 0; */ > > *result = sqrt(x1+x2); > } > > I have two questions: > > - this seems to show the necessary cooperation of the value plugin and > the wp plugin but it is not clear to me why such a cooperation is > needed, can you give me some hints to understand why the wp plugin > alone cannot validate the sqrt precondition and why the value plugin > is unable to validate the inserted assertions ? More generally, > should we explore the function expression tree to insert intermediate > variables with assertions on known facts that may probably be > verifiable by only the wp plugin ? > > - the alt-ergo file for the second assertion is not the same as the > first one. I understand that the first assertion is "embeded" in > the second one (*). How to "isolate" each assertion from the other > one, or in other words, how to tell frama-c and the external > provers that, for me and the problem I consider, the order of > computation of x1 and x2 does not matter ? > > > Regards, > > Maurice Bremond > > > (*) the alt-ergo files for the 2 assertions: > > (* ---------------------------------------------------------- *) > (* --- Assertion (file t.c, line 23) --- *) > (* ---------------------------------------------------------- *) > > goal f_assert: > forall r_1,r : real. > let r_2 = (r_1 * r_1) : real in > ((-1000000.0e0) <= r) -> > ((-1000000.0e0) <= r_1) -> > (r <= 1000000.0e0) -> > (r_1 <= 1000000.0e0) -> > is_float64(r) -> > is_float64(r_1) -> > is_float64(r_2) -> > (0.0 <= r_2) > > > (* ---------------------------------------------------------- *) > (* --- Assertion (file t.c, line 26) --- *) > (* ---------------------------------------------------------- *) > > goal f_assert_2: > forall r_1,r : real. > let r_2 = (r_1 * r_1) : real in > let r_3 = (r * r) : real in > ((-1000000.0e0) <= r) -> > ((-1000000.0e0) <= r_1) -> > (r <= 1000000.0e0) -> > (r_1 <= 1000000.0e0) -> > is_float64(r) -> > is_float64(r_1) -> > (0.0 <= r_2) -> > is_float64(r_3) -> > is_float64(r_2) -> > (0.0 <= r_3) > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://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/20160421/b4c90845/attachment-0001.html>

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

- Prev by Date:
**[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin** - Next by Date:
**[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin** - Previous by thread:
**[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin** - Next by thread:
**[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin** - Index(es):