Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000691Frama-CKernel > ACSL implementationpublic2011-01-27 14:052014-02-12 16:59
Reporterlukaszc 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000691: Comments parsing not always work
Description/*@ lemma fib_3: fib(3) == 2; // proved automatically */
/*@ lemma fib_46: fib(46) == 1836311903; */

generates only one verification condition in jessie, i.e. for fig_46. However,
/*@ lemma fib_3: fib(3) == 2; */ /* proved automaticall */
/*@ lemma fib_46: fib(46) == 1836311903; */
works properly generating 2 VC, i.e. fib_3 and fib_46
TagsNo tags attached.
Attached Files

- Relationships
has duplicate 0000812closedvirgile Cil does not correctly handle ACSL annotations with nested comments when called with -pp-annot 

-  Notes
(0001429)
virgile (developer)
2011-01-27 19:06

The issue is due to -pp-annot (which Jessie always set to true for reasons known only to itself)
(0004796)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-01-27 14:05 lukaszc New Issue
2011-01-27 14:05 lukaszc Status new => assigned
2011-01-27 14:05 lukaszc Assigned To => cmarche
2011-01-27 18:28 signoles Assigned To cmarche => virgile
2011-01-27 18:28 signoles Category Plug-in > jessie => Kernel > ACSL implementation
2011-01-27 19:06 virgile Note Added: 0001429
2011-01-27 19:06 virgile Status assigned => acknowledged
2011-05-03 22:23 virgile Relationship added has duplicate 0000812
2011-05-06 16:35 svn Checkin
2011-05-06 16:35 svn Status acknowledged => resolved
2011-05-06 16:35 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004796
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker