Frama-C Bug Tracking System - Frama-C
View Issue Details
0001836Frama-CPlug-in > E-ACSLpublic2014-07-16 11:142014-09-15 17:20
arvidj 
signoles 
normalminorsometimes
closedfixed 
 
Frama-C Neon-20140301 
0001836: A pointer can be reported as belonging to an adjacent memory blocks in the bittree memory model
There is a one-off error in the calculation of to which block a pointer. The following series of calls to the memory model triggers it (but I've got no simple program example which reproduces the error). struct _block bk1 = {.ptr = 1, .size = 1}; __add_element(&bk1); assert(__get_cont((void*)0) == NULL); assert(__get_cont((void*)1) == &bk2); assert(__get_cont((void*)2) == NULL); // will report 2 as belonging to bk1. The offending line in e_acsl_bittree.c is: else if((size_t)ptr <= tmp->leaf->size + tmp->addr) where the comparison is strict and another clause should be added to handle the case of empty structs.
No tags attached.
Issue History
2014-07-16 11:14arvidjNew Issue
2014-07-16 11:14arvidjStatusnew => assigned
2014-07-16 11:14arvidjAssigned To => signoles
2014-07-16 11:21signolesStatusassigned => acknowledged
2014-07-19 18:30signolesStatusacknowledged => resolved
2014-07-19 18:30signolesResolutionopen => fixed
2014-09-15 17:20signolesFixed in Version => Frama-C Neon-20140301
2014-09-15 17:20signolesNote Added: 0005456
2014-09-15 17:20signolesStatusresolved => closed

Notes
(0005456)
signoles   
2014-09-15 17:20   
Fixed in E-ACSL v0.4.1.