Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000643Frama-CKernel > ACSL implementationpublic2010-12-17 18:012010-12-18 11:23
ReporterAstra 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000643: Incorrect parsing of complex lemma
DescriptionWhen 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.
TagsNo tags attached.
Attached Filesc file icon qsorti.c [^] (22,630 bytes) 2010-12-17 18:01 [Show Content]

- Relationships

-  Notes
(0001329)
cmarche (developer)
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
(0001330)
pascal (reporter)
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 http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [^] 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.

- Issue History
Date Modified Username Field Change
2010-12-17 18:01 Astra New Issue
2010-12-17 18:01 Astra Status new => assigned
2010-12-17 18:01 Astra Assigned To => cmarche
2010-12-17 18:01 Astra File Added: qsorti.c
2010-12-17 20:20 cmarche Note Added: 0001329
2010-12-17 20:20 cmarche Assigned To cmarche => virgile
2010-12-18 00:33 pascal Note Added: 0001330
2010-12-18 11:23 signoles Category Plug-in > jessie => Kernel > ACSL implementation


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker