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: Maurice.Bremond at inria.fr (Maurice Bremond)
  • Date: Thu, 21 Apr 2016 16:34:17 +0200
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)