Incorrect parsing of complex lemma
ID0000643: This issue was created automatically from Mantis Issue 643. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000643 | Frama-C | Kernel > ACSL implementation | public | 2010-12-17 | 2010-12-18 |
| Reporter | Astra | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
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 inta, 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.