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