Frama-C Bug Tracking System - Frama-C
View Issue Details
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

Notes
(0001051)
virgile   
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
2010-06-17 18:18JochenNew Issue
2010-06-18 08:36signolesStatusnew => assigned
2010-06-18 08:36signolesAssigned To => virgile
2010-06-18 08:39virgileStatusassigned => acknowledged
2010-08-17 18:39virgileNote Added: 0001051
2010-08-18 10:45svn
2010-08-18 10:45svnStatusacknowledged => resolved
2010-08-18 10:45svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed
2013-12-19 01:12Source_changeset_attached => framac master eb164ca5
2014-02-12 16:55Source_changeset_attached => framac stable/neon eb164ca5