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