Literal strings can be added multiple times in memory
ID0001837: This issue was created automatically from Mantis Issue 1837. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001837 | Frama-C | Plug-in > E-ACSL | public | 2014-07-16 | 2015-06-08 |
| Reporter | arvidj | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Sodium |
Description :
Consider the following example:
int i = 4; while (i--) { char *s = "toto"; /@ assert \valid(s) ; */ printf(s); }
Each time the body of the while-loop is executed, the block corresponding to "toto" is added to the memory store, however this string has always the same address.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information