Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 02:44 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002252Frama-CPlug-in > E-ACSLpublic2017-05-31 19:05
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSGentooOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFrama-C GIT, precise the release idFixed in VersionFrama-C 15-Phosphorus 
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 Files
  • c file icon bts2252.c (470 bytes) 2017-01-25 16:40 -
    /* run.config
       COMMENT: bts #2252, failures due to typing of offsets
    */
    
    #include <stdlib.h>
    
    int main() {
    	char* srcbuf="Test Code";
    	int i, loc = 1;
    
    	char * destbuf = (char*)malloc(10*sizeof(char));
    	char ch = 'o';
    
    	if(destbuf!=NULL) {
    		for (i = -1; i < 10; i++) {
          /*@ assert \valid_read(srcbuf + i); */
          if(srcbuf[i]==ch) { /* ERROR: Buffer Underrun */
            loc=i;
          }
        }
        strncpy(&destbuf[loc], &srcbuf[loc], 1);
        free(destbuf);
    	}
    }
    
    c file icon bts2252.c (470 bytes) 2017-01-25 16:40 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-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
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
+Issue History