2021-01-27 11:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001022Frama-CDocumentation > ACSLpublic2016-01-26 08:52
ReporterJochen 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0001022: suggest to explain semantics of missing loop assigns clause in Acsl manual
DescriptionIn the manual "ACSL: ANSI/ISO C Specification Language, Version 1.5", on p.35-36, the semantics of a loop assigns clause is explained. On p.34, the default for a missing assigns clause in a function contract is explained.

However, the default for a missing loop assigns clause seems to remain unexplained in the manual.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006029

patrick (developer)

If no loop assigns clause is given, assignments remain unspecified.
It is left to tools to compute an over-approximation of the sets
of assigned locations.

~0006030

patrick (developer)

That text has been added into ACSL manual.
+Notes

-Issue History
Date Modified Username Field Change
2011-11-18 15:49 Jochen New Issue
2011-11-18 15:49 Jochen Status new => assigned
2011-11-18 15:49 Jochen Assigned To => signoles
2011-11-18 18:56 signoles Assigned To signoles => virgile
2015-09-07 15:29 signoles Assigned To virgile => patrick
2015-09-09 14:26 patrick Note Added: 0006029
2015-09-09 14:26 patrick Note Added: 0006030
2015-09-18 07:34 patrick Status assigned => resolved
2015-09-18 07:34 patrick Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History