Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000512Frama-CKernelpublic2010-06-17 18:182014-02-12 16:55
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeveritytrivialReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000512: suggest to refer to fct-contract's clauses-order in error message
DescriptionIf the clauses-order (specified in Fig.2.4 (p.27) of the document "ACSL Version 1.4 / Implementation in Boron-20100401") is violated by a program, the kernel just reports "user error: syntax error while parsing annotation". I suggest to replace that rather general message by a more specific like e.g. "decreases-clause after ensures-clauses not allowed in function contract".

Similarly, a message like "decreases-clause missing for recursive function" rather than tacitly generating an unsatisfiable proof goal "... ==> 0<0" would be helpful.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001051)
virgile (developer)
2010-08-17 18:39

the warning for missing decrease clause is specific to Jessie/Why. No clause is generated by the Jessie plugin itself. Thus Why should generate the warning (when in total mode).

- Issue History
Date Modified Username Field Change
2010-06-17 18:18 Jochen New Issue
2010-06-18 08:36 signoles Status new => assigned
2010-06-18 08:36 signoles Assigned To => virgile
2010-06-18 08:39 virgile Status assigned => acknowledged
2010-08-17 18:39 virgile Note Added: 0001051
2010-08-18 10:45 svn Checkin
2010-08-18 10:45 svn Status acknowledged => resolved
2010-08-18 10:45 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker