Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000812Frama-CKernel > ACSL implementationpublic2011-05-03 22:012011-10-10 14:14
Reporteryakobowski 
Assigned Tovirgile 
PrioritylowSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000812: Cil does not correctly handle ACSL annotations with nested comments when called with -pp-annot
DescriptionCalling frama-c with -pp-annot on the two codes below results in a crash (first code), or a not so clear message (second code).

--- Code 1 ----

/*@ assigns \nothing;
// Bla */
void main() {
}


--- Code 2 ----

/*@ assigns \nothing;
// Bla */
void main() {
}

/* */
TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0000691closedvirgile Comments parsing not always work 

-  Notes
(0001849)
virgile (developer)
2011-05-06 16:36

fixed in rev 13329

- Issue History
Date Modified Username Field Change
2011-05-03 22:01 yakobowski New Issue
2011-05-03 22:02 yakobowski Status new => assigned
2011-05-03 22:02 yakobowski Assigned To => virgile
2011-05-03 22:23 virgile Relationship added duplicate of 0000691
2011-05-03 22:24 virgile Category Kernel => Kernel > ACSL implementation
2011-05-06 16:36 virgile Note Added: 0001849
2011-05-06 16:36 virgile Status assigned => resolved
2011-05-06 16:36 virgile Fixed in Version => Frama-C GIT, precise the release id
2011-05-06 16:36 virgile Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version Frama-C GIT, precise the release id => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker