--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on November 2013 ---
[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                    |