# 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*: Thu, 21 Apr 2016 18:13:22 +0200*In-reply-to*: <87k2jrkp3q.fsf@inria.fr>*References*: <87k2jrkp3q.fsf@inria.fr>

Hello, I'm going to complement LoÃ¯c's answer by explaining how to set up Value so that everything gets proven automatically. Value is not able to prove the precondition of sqrt because f computes a non-linear expression (x*x+y*y). This kind of expression cannot be analysed precisely by the interval analysis that Value uses for floating-point values. That being said, an option is available to improve precision on such formulas: -val-subdivide-non-linear. This option instructs Value to subdivide variables that appear multiple times in an expression into a disjoint union of intervals, and to perform the evaluation pointwise. By setting N high enough, it becomes possible to prove that e.g. x*x is always positive. The option was originally named -subdivide-float-var, but was renamed because it now also applies to integers. You will find more information on the original option there: http://blog.frama-c.com/index.php?q=subdivide. Regarding the expressiveness of this option, the current versions of Frama-C are not able to handle expressions that are non-linear on multiple variables, such as x*x+y*y. Support for these expressions will be available in Frama-C Silicon, though. (We actually added this support in the last month.) The current versions of Value are able to prove your second version of f (with intermediate variables), because each temporary is linear on one variable. Finally, notice there exists a Value builtin for sqrt, that can be activated through option -val-builtin sqrt:Frama_C_sqrt. This way, you will get tighter bounds for the results of sqrt. For technical reasons, this builtin does *not* check the preconditions present in the source, but verify by itself the domain of its argument. Hope this helps! On Thu, Apr 21, 2016 at 4:34 PM, Maurice Bremond <Maurice.Bremond at inria.fr> wrote: > > 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 -- Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160421/899fddd1/attachment.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] Contract status dependences** - 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):