--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2016 ---
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>