suggest to explain semantics of missing loop assigns clause in Acsl manual
ID0001022: This issue was created automatically from Mantis Issue 1022. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001022 | Frama-C | Documentation > ACSL | public | 2011-11-18 | 2016-01-26 |
| Reporter | Jochen | Assigned To | patrick | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Magnesium |
Description :
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information