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] label L required?

  • Subject: [Frama-c-discuss] label L required?
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Thu, 31 Oct 2013 13:42:48 -0400
I can use Frama-C+Jessie+Z3 to verify the program below.  However, if I remove all the "{L}"s from the specification, I get the following error:

[jessie] Calling Jessie tool in subdir mean2b.jessie
File "mean2b.jc", line 44, characters 2-173: typing error: there should be at least one declared symbol depending on label L in this axiom
[jessie] user error: Jessie subprocess failed:   jessie  -why3ml  -v       -locs mean2b.cloc mean2b.jc

There is no label L in the source (since I removed them), but in the intermediate file mean2b.jc, an "{L}" was added to axiom sum1:

---

axiomatic sums {

  logic real sum(doubleP[..] a, integer n)
   
  axiom sum0 :
  (\forall doubleP[..] a_0;
    (sum(a_0, 0) == 0.0))
   
  axiom sum1{L} :
  (\forall doubleP[..] a_1;
    (\forall integer n_0;
      ((n_0 >= 1) ==>
        (sum(a_1, n_0) == (sum(a_1, (n_0 - 1)) + (a_1 + (n_0 - 1)).doubleM)))))
---

Does anyone know, why this happened?  It didn't happen to sum0, and it doesn't happen in other similar examples I have tried.

Do I have to put in all the "{L}" in the source file?

Thanks,
Steve


---

# pragma JessieIntegerModel(math)
# pragma JessieFloatModel(math)

/*@ axiomatic sums {
  @   logic real sum{L}(double *a, integer n);
  @   axiom sum0{L}: \forall double *a; sum{L}(a,0)==0.0;
  @   axiom sum1{L}: \forall double *a, integer n; n>=1 ==> 
  @     sum{L}(a,n)==sum{L}(a,n-1)+a[n-1];
  @ }
  @*/


/*@ requires n >= 1 && \valid(t+(0..n-1));
  @ ensures \result == 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;
}

---