Opened 5 weeks ago

Last modified 3 weeks ago

#35 new feature

Track origins of memory objects.

Reported by: mornfall Owned by:
Priority: major Milestone: 5.0
Component: DiOS Keywords:
Cc:

Description

With #32, it should be easy to attach a stack trace (probably just a vector of program counters) to each memory object (possibly using some form of --autotrace allocs). Along with #33 and #34, this would make it possible to provide nice leak reports, including origin information. Since the book-keeping would be hidden under dbg.call, this should not slow down model checking (though it will increase the cost of generating the counterexample trace).

Change History (1)

comment:1 Changed 3 weeks ago by mornfall

Milestone: future5.0

Milestone renamed

Note: See TracTickets for help on using tickets.