2021-03-01 05:27 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000512Frama-CKernelpublic2014-02-12 16:55
Assigned Tovirgile 
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




virgile (developer)

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
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
2013-12-19 01:12 Source_changeset_attached => framac master eb164ca5
2014-02-12 16:55 Source_changeset_attached => framac stable/neon eb164ca5
+Issue History