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

  • Subject: [Frama-c-discuss] Jessie: unbound symbol round_double_logic
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Fri, 1 Nov 2013 09:50:32 -0400
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