Frama-C Bug Tracking System - Frama-C
View Issue Details
0000643Frama-CKernel > ACSL implementationpublic2010-12-17 18:012010-12-18 11:23
Frama-C Boron-20100401 
0000643: Incorrect parsing of complex lemma
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.
No tags attached.
c qsorti.c (22,630) 2010-12-17 18:01
Issue History
2010-12-17 18:01AstraNew Issue
2010-12-17 18:01AstraStatusnew => assigned
2010-12-17 18:01AstraAssigned To => cmarche
2010-12-17 18:01AstraFile Added: qsorti.c
2010-12-17 20:20cmarcheNote Added: 0001329
2010-12-17 20:20cmarcheAssigned Tocmarche => virgile
2010-12-18 00:33pascalNote Added: 0001330
2010-12-18 11:23signolesCategoryPlug-in > jessie => Kernel > ACSL implementation

2010-12-17 20:20   
First this has nothing to do with Jessie, the error is raised by the kernel. (Please do not assign a bug by yourself, let the BTS admin do it) The reason of the error message are the array acccess lbstack[i] and such: it is not know in which memory state : use \at(..., L1) or \at(..,L2). So it is not a bug, just a not enough precise error message
2010-12-18 00:33   
To clear up a misunderstanding, the only thing the reporter is guilty of here is having chosen category "Jessie" for a bug that can be reproduced with "frama-c qsorti.c" (modulo the trickery to expand macros in annotations and removal of #include directive). Bug categories are intended to be picked by reporters. Claude, if you do not like being auto-assigned Jessie bugs, I invite you to complain to the BTS admin. We would have a right to complain for miscategorized bugs if explained, in the paragraph about CATEGORY, how to categorize a bug as a kernel bug. It doesn't, but good news! It's a wiki, so anyone can add the information there.