Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002252Frama-CPlug-in > E-ACSLpublic2016-10-14 17:372017-01-25 18:11
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSGentooOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFrama-C GIT, precise the release idFixed in Version 
Summary0002252: GMP typing issue
DescriptionIn 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.

TagsNo tags attached.
Attached Filesc file icon bts2252.c [^] (470 bytes) 2017-01-25 16:40 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker