--- layout: fc_discuss_archives title: Message 1 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



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