\initialized applied to non-pointer in acsl-manual
ID0001371: This issue was created automatically from Mantis Issue 1371. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001371 | Frama-C | Documentation > ACSL | public | 2013-02-18 | 2013-02-28 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | no change required |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | - |
Description :
The manual "acsl.pdf", p.66-67 says:
int f(int n) { int x; if (n > 0) x = n ; else x = -n; //@ assert \initialized(x); return x; }
However, this code is not accepted by kernel; after changing the argument of \initialized from "x" to "&x", it is accepted. The manual text should be corrected accordingly.