--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on October 2013 ---
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; } ---