Valid access to literal w_chart string address considered invalid
ID0000949: This issue was created automatically from Mantis Issue 949. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000949 | Frama-C | Plug-in > Eva | public | 2011-09-02 | 2011-10-10 |
| Reporter | monate | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | Frama-C GIT, precise the release id | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
#include <stddef.h>
int main() {
// String literals are lvalues char (*p)[4] = &("bar"); wchar_t (*q)[4] = &(L"foO");
if((*p)[1] != 'a') return 1; if((*q)[1] != 'o') return 2;
return 0; }
return 0 when gcc'ed but frama-c -val ends with tests/cil/string.c:10:[kernel] warning: out of bounds read. assert \valid(&(*q)[1]);