Frama-C Bug Tracking System - Frama-C
View Issue Details
0000691Frama-CKernel > ACSL implementationpublic2011-01-27 14:052014-02-12 16:59
lukaszc 
virgile 
normalmajoralways
closedfixed 
Frama-C Carbon-20101202-beta2 
Frama-C Nitrogen-20111001 
0000691: Comments parsing not always work
/*@ 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
No tags attached.
has duplicate 0000812closed virgile Cil does not correctly handle ACSL annotations with nested comments when called with -pp-annot 
Issue History
2011-01-27 14:05lukaszcNew Issue
2011-01-27 14:05lukaszcStatusnew => assigned
2011-01-27 14:05lukaszcAssigned To => cmarche
2011-01-27 18:28signolesAssigned Tocmarche => virgile
2011-01-27 18:28signolesCategoryPlug-in > jessie => Kernel > ACSL implementation
2011-01-27 19:06virgileNote Added: 0001429
2011-01-27 19:06virgileStatusassigned => acknowledged
2011-05-03 22:23virgileRelationship addedhas duplicate 0000812
2011-05-06 16:35svnCheckin
2011-05-06 16:35svnStatusacknowledged => resolved
2011-05-06 16:35svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004796
2014-02-12 16:59Statusclosed => resolved

Notes
(0001429)
virgile   
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.