| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0002114 | Frama-C | Documentation > ACSL | public | 2015-05-05 17:29 | 2016-01-26 08:52 | ||||
| Reporter | dcok@grammatech.com | ||||||||
| Assigned To | patrick | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Sodium | ||||||||
| Target Version | Frama-C Magnesium | Fixed in Version | Frama-C Magnesium | ||||||
| Summary | 0002114: ACSL manual:issues affecting technical correctness or understanding | ||||||||
| Description | These are issues affecting technical correctness or understanding that I encountered in a recent read through of the ACSL 1.9 manual. p. 27: There are extraneous { delimiters in the example. p. 51/52, Example 2.42: Either line 3 of the example should have ? (n-1) :" instead of "? n :" or the explanation should be corrected. p. 56, Example 2.47: "modifies t[k]" -> "only modifies t[k]" p. 57: "where the file list.acsl contains logic definitions" -> "where the file List.acsl contains logic definitions" - at least I presume the name of the file must be a case-senstive match to the name of the module p. 58: "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)))" should be "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)-1))" and similarly for \valid_read p. 71, Example 2.59: These specs allow forbidden to have more values than the union of {\result} and \old(forbidden) p. 72: In "It is however possible to write multi-line annotations for ghost code. These annotations are enclosed between /@ and @/. As in normal annotations, @s at the beginning of a line and at the end of the comment (before the final @/) are considered as blank." the /@ and @/ should be /*@ and @*/ | ||||||||
| Steps To Reproduce | Read the documentation | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
dcok@grammatech.com (reporter) 2015-05-05 17:36 |
One more: p. 27: The statement "Beware that equality of unions is also equality of all fields." deserves some explanation. It is equality of all fields, even if they overlap - so not just equality of the last assignment. If it is equality of all fields, then the example just above ought to be true. |
|
patrick (developer) 2015-09-07 10:18 |
all accepted except: p.27 "There are extraneous { delimiters in the example." -> Extraneous { was not found? p. 72 "... the /@ and @/ should be /*@ and @*/" -> No, because the C preprocessor closes alls /*@ when it reaches the first @*/ p. 27 "... If it is equality of all fields, then the example just above ought to be true." -> No, for the union type the equality is false. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2015-05-05 17:29 | dcok@grammatech.com | New Issue | |
| 2015-05-05 17:29 | dcok@grammatech.com | Status | new => assigned |
| 2015-05-05 17:29 | dcok@grammatech.com | Assigned To | => signoles |
| 2015-05-05 17:33 | signoles | Assigned To | signoles => virgile |
| 2015-05-05 17:33 | signoles | Target Version | => Frama-C Magnesium |
| 2015-05-05 17:36 | dcok@grammatech.com | Note Added: 0005911 | |
| 2015-09-04 10:50 | bobot | Assigned To | virgile => patrick |
| 2015-09-07 10:18 | patrick | Note Added: 0006022 | |
| 2015-09-07 10:29 | patrick | Status | assigned => resolved |
| 2015-09-07 10:29 | 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 |