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] Jessie: unbound symbol round_double_logic

Hi,

This is indeed a bug, cast to double in logic was supported by the Why2
backend (thus you can still deal with this program using frama-c -jessie
-jessie-atp=gui) that was not ported to the Why3 back-end.

This should be fixed in the next release of Why2/Jessie. In the
mean-time, you can replace cast to double as follows: replace each

(double)e

by

\round_float(\Double,\NearestEven,e)

Sorry for the inconvenience.

- Claude

Le 01/11/2013 14:50, Stephen Siegel a ?crit :
> 
> /*@ axiomatic sums {
>   @   logic real sum{L}(double *a, integer n);
>   @   axiom sum1{L}: \forall double *a, integer n; n>=1 ==> 
>   @     sum{L}(a,n)==(double)(sum{L}(a,n-1)+a[n-1]);
>   @   axiom sum0{L}: \forall double *a; sum{L}(a,0)==0.0;
>   @ }
>   @*/
> 
> /*@ requires n >= 1 && \valid(t+(0..n-1));
>   @ ensures \result == (double)(sum(t,n)/n);
>   @ assigns \nothing;
>   @*/
> double mean(double *t, int n) {
>   int i;
>   double s = 0.0;
> 
>   /*@ loop invariant 0<=i<=n;
>     @ loop invariant \valid(t+(0..n-1));
>     @ loop invariant s==sum(t,i);
>     @ loop assigns s;
>     @ loop variant n-i;
>     @*/
>   for (i=0; i<n; i++) 
>     s += t[i];
>   return s/n;
> }

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |