2021-01-27 11:12 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001022Frama-CDocumentation > ACSLpublic2016-01-26 08:52
Assigned Topatrick 
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




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.


patrick (developer)

That text has been added into ACSL manual.

-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