Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 01:57 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000691Frama-CKernel > ACSL implementationpublic2014-02-12 16:59
Reporterlukaszc 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 
+Relationships

-Notes

~0001429

virgile (developer)

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

~0004796

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:12 Source_changeset_attached => framac master 958cefa3
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 958cefa3
2014-02-12 16:59 Note Added: 0004796
2014-02-12 16:59 Status closed => resolved
+Issue History