Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001836Frama-CPlug-in > E-ACSLpublic2014-07-16 11:142014-09-15 17:20
Reporterarvidj 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilitysometimes
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001836: A pointer can be reported as belonging to an adjacent memory blocks in the bittree memory model
DescriptionThere 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005456)
signoles (manager)
2014-09-15 17:20

Fixed in E-ACSL v0.4.1.

- Issue History
Date Modified Username Field Change
2014-07-16 11:14 arvidj New Issue
2014-07-16 11:14 arvidj Status new => assigned
2014-07-16 11:14 arvidj Assigned To => signoles
2014-07-16 11:21 signoles Status assigned => acknowledged
2014-07-19 18:30 signoles Status acknowledged => resolved
2014-07-19 18:30 signoles Resolution open => fixed
2014-09-15 17:20 signoles Fixed in Version => Frama-C Neon-20140301
2014-09-15 17:20 signoles Note Added: 0005456
2014-09-15 17:20 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker