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.