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] EVA postcondition propagation

  • Subject: [Frama-c-discuss] EVA postcondition propagation
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Sun, 2 Jul 2017 11:58:15 +0200
  • In-reply-to: <13e5-594bcb80-33b-1f2204c0@207214991>
  • References: <13e5-594bcb80-33b-1f2204c0@207214991>
Hi,

Thanks for the interesting question, and apologies for the late answer --
which is going to be a bit involved. The root of your problem is an
insufficient modeling. But you also encountered a bug, plus something we
would like to improve.

## Insufficient modeling

The WP plugin is quite happy with 'assigns' clauses, and the ACSL
specification puts emphasis mostly on those kind of clauses. However, EVA
needs more. More precisely, '\from' clauses, which document the "origin" of
the value which is being written, are required. This is documented
extensively in section 7.2 of the EVA manual. In your case, if `foo` and
`foo_d` read nothing to compute their results, the required specification
is simply

/*@
  @ assigns \result \from \nothing;
  @ ensures \result == 1.0f;
  @*/
float foo();

Notice that EVA complains (loudly) when you specify an 'assigns' clause
without a '\from'.

postcond.c:6:[value] warning: no 'assigns \result \from ...' clause
specified for function foo


## Wait, the results are even worse this way

If you modify your code according to my suggestion, you will notice that
none of the postconditions have an effect anymore. Furthermore, both x and
y receive a value ([--..--]) which is quite imprecise: it includes all
possible floating-point values, but also infinites and NaNs. For technical
reasons, that we hope to remove soon, it is currently not possible to
reduce by a postcondition on such an imprecise value. The solution is to
require the result to be finite _before_ constraining it.

/*@
  @ assigns \result \from \nothing;
  @ ensures \is_finite(\result);
  @ ensures \result == 1.0f;
  @*/
float foo();

With those changes, the analysis performs as expected.


## Ok, but why the difference between foo and foo_d in the original code?

The value assigned to x in your original code is the result of a bug. A 32
bits floating-point value should never be assigned a value that only fits
in 64 bits. Because of this bug, EVA detected an overflow, and refused to
perform the reduction by the postcondition. Once the bug is fixed, both
functions return the precise result {1.}.

Hope this helps,


On Thu, Jun 22, 2017 at 3:52 PM, CLAVIERE Arthur <
Arthur.CLAVIERE at student.isae-supaero.fr> wrote:

> When using a specification instead of a function, it seems that EVA
> propagates postconditions for double variables but not for float variables.
> With the following example, we obtain :
> x in [-1.79769313486e+308 .. 1.79769313486e+308]
> y in {1.}
>
> /*@
>   @ assigns \nothing;
>   @ ensures \result == 1.0f;
>   @*/
> float foo();
>
> /*@
>   @ assigns \nothing;
>   @ ensures \result == 1.0;
>   @*/
> double foo_d();
>
> int main(int argc, char *argv[])
> {
>     float  x = foo();
>     double y = foo_d();
>
>     return 0;
> }
>
>
>
> Regards,
>
> Arthur
>
> --
>
>
>
> Arthur CLAVIÈRE
> Elève ingénieur SUPAERO - 2A
>
> ISAE SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace
> 10 avenue Edouard Belin - BP 54032 - 31055 TOULOUSE CEDEX 4 FRANCE -
> http://www.isae-supaero.fr
> Tel +33 5 61 33 80 80 <+33%205%2061%2033%2080%2080> - Fax (+33) 5 61 33
> 83 30 <+33%205%2061%2033%2083%2030>
> Plan d'accès/Access map <http://plan.univ-toulouse.fr/#783>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://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/20170702/29721731/attachment.html>