Frama-C Bug Tracking System - Frama-C
View Issue Details
0001022Frama-CDocumentation > ACSLpublic2011-11-18 15:492016-01-26 08:52
Jochen 
patrick 
normaltextN/A
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Magnesium 
0001022: suggest to explain semantics of missing loop assigns clause in Acsl manual
In 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.
No tags attached.
Issue History
2011-11-18 15:49JochenNew Issue
2011-11-18 15:49JochenStatusnew => assigned
2011-11-18 15:49JochenAssigned To => signoles
2011-11-18 18:56signolesAssigned Tosignoles => virgile
2015-09-07 15:29signolesAssigned Tovirgile => patrick
2015-09-09 14:26patrickNote Added: 0006029
2015-09-09 14:26patrickNote Added: 0006030
2015-09-18 07:34patrickStatusassigned => resolved
2015-09-18 07:34patrickResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL

Notes
(0006029)
patrick   
2015-09-09 14:26   
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   
2015-09-09 14:26   
That text has been added into ACSL manual.