--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on November 2013 ---
I am trying to apply Frama-C+Jessie to the program below. Things go fine until the Why3 IDE opens up. Then Why3 reports an error in a popup window: Error while reading file '../mean3.mlw': File "mean3/../mean3.mlw", line 284, characters 48-66: Unbound symbol 'round_double_logic' I am using casts from real to (double) in the spec, which I know uses round_double. Am I supposed to #include a header file or something like that? Thanks, Steve /*@ 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; } mean$ frama-c -jessie mean3.c [kernel] preprocessing with "gcc -C -E -I. -dD mean3.c" [jessie] Starting Jessie translation [jessie] Producing Jessie files in subdir mean3.jessie [jessie] File mean3.jessie/mean3.jc written. [jessie] File mean3.jessie/mean3.cloc written. [jessie] Calling Jessie tool in subdir mean3.jessie Generating Why function mean [jessie] Calling VCs generator. why3ide --extra-config /Users/siegel/.opam/4.00.1/lib/why/lib/why/why3/why3.conf mean3.mlw [Info] Init the GTK interface... done. [Info] reading icons... done. [Info] Creating tree model... done [Info] found regular file 'mean3.mlw' [Info] using 'mean3' as directory for the project [Info] Opening session... [Info] Opening session: update done [Info] Opening session: done Adding file '../mean3.mlw' [Info] adding file ../mean3.mlw in database [Info] saving IDE config file