Opened 2 years ago

Last modified 2 years ago

#16 new feature

Undetected double free

Reported by: Henrich Lauko Owned by: Henrich Lauko
Priority: major Milestone: 5.0
Component: LART Keywords:


In current divine, we are not able to detect possible double free here.

  #include <stdlib.h>
  int main() {
      void *x = malloc(0x1000);
      void *y = malloc(0x1000);
      if (x == y)

Is there a way we would be able to do that?

Change History (3)

comment:1 Changed 2 years ago by mornfall

This is pretty much a use-case for the pointer domain described in the medium-term roadmap, where objid's are symbolic in numeric contexts but explicit in pointer contexts. There would be some fiddling to do with lifetime overlaps, since we may need to maintain a number of constraints on such symbolic object identifiers (namely that they are distinct from each other if the object lifetimes overlap). This may be a little annoying, but i don't imagine it's a showstopper.

comment:2 Changed 2 years ago by mornfall

Milestone: future5.0

Milestone renamed

comment:3 Changed 2 years ago by mornfall

Component: VMLART
Owner: changed from mornfall to Henrich Lauko
Type: defectfeature
Note: See TracTickets for help on using tickets.