--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] label L required?



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;
}

---