View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002252 | Frama-C | Plug-in > E-ACSL | public | 2016-10-14 17:37 | 2017-05-31 19:05 | ||||
Reporter | kvorobyov | ||||||||
Assigned To | signoles | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | Gentoo | OS Version | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Frama-C GIT, precise the release id | Fixed in Version | Frama-C 15-Phosphorus | ||||||
Summary | 0002252: GMP typing issue | ||||||||
Description | In the below snippet 1 int i = -1; 2 ... 3 /*@ assert rte: mem_access: \valid_read(srcbuf+i); */ 4 if ((int)*(srcbuf + i) == (int)ch) 5 loc = i; a buffer overflow occurs because of the initial negative value of i, however, assertion generated by E-ACSL features the following line: __e_acsl_valid_read((void *)(srcbuf + (unsigned long)i), sizeof(char)); which casts i to an unsigned integer and further make the assertion wrongly pass. See the attached code for a more complete example. The code is taken from the ITC toyota benchmark. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2016-10-14 17:37 | kvorobyov | New Issue | |
2016-10-14 17:37 | kvorobyov | Status | new => assigned |
2016-10-14 17:37 | kvorobyov | Assigned To | => signoles |
2016-10-14 17:37 | kvorobyov | File Added: var.frama-c.i | |
2017-01-19 16:56 | signoles | Status | assigned => resolved |
2017-01-19 16:56 | signoles | Resolution | open => fixed |
2017-01-19 16:56 | signoles | Status | resolved => closed |
2017-01-19 16:57 | signoles | Status | closed => assigned |
2017-01-25 16:39 | kvorobyov | File Deleted: var.frama-c.i | |
2017-01-25 16:40 | kvorobyov | File Added: bts2252.c | |
2017-01-25 18:11 | kvorobyov | Status | assigned => resolved |
2017-05-31 19:04 | signoles | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:05 | signoles | Status | resolved => closed |