Description | When I try to run jessie for the attached file, I get the next message:
[kernel] preprocessing with "gcc -C -E -I. -dD qsorti.c"
qsorti.c:267:[kernel] user error: Error during annotations analysis: no label in the context. (\at or explicit label missing?)
The 267th line:
@ ==> ((0 <= lbstack[i] <= ubstack[i] <= lbstack[i+1] <= ubstack[i+1] <= lb <= ub <= size-1)
and lemma:
/*@lemma hole_sameArray_stack{L1,L2} :
@ (\forall int*a, int* lbstack, int* ubstack, integer pos, integer lb, integer ub, integer size;
@ (\forall integer i; 1 <= i < pos
@ ==> (0 <= lbstack[i] <= ubstack[i] <= lbstack[i+1] <= ubstack[i+1] <= lb <= ub <= size-1
@ && good_hole{L1}(a, lbstack, ubstack, i, size)
@ && sameArray{L1,L2}(a, size, lb, ub)))
@ ==>
@ (\forall integer j; (1 <= j < pos
@ ==> good_hole{L2}(a, lbstack, ubstack, j, size))));
*/
predicate:
/*@ predicate good_hole{L}(int* a, int* lbstack, int* ubstack, integer i, integer size) =
@ is_sorted{L}(a, ubstack[i], lbstack[i+1])
@ && left_part_less{L}(a, ubstack[i]+1, lbstack[i], lbstack[i+1]-1)
@ && left_part_less{L}(a, lbstack[i+1]-1, ubstack[i]+1, size-1);
*/
There are some similar lemmas with such labels and no error was occur with them. |