Opened 17 months ago

#90 new defect

VFS: Divine segfaults while loading when capturing a diffutils directory

Reported by: Lukáš Zaoral Owned by:
Priority: major Milestone: 4.3
Component: DiOS Keywords:
Cc: kdudka@…, jamartis@…, lzaoral@…


the following issue still persists even with the latest VFS patches in the next branch. The reproduction is a bit cumbersome, but I was not able to find a smaller example than this.

  1. Download the latest upstream version of diffutils and extract it.
  2. Configure and compile this version with dioscc. The compilation won't complete, but at least the cmp binary will be created.
  3. Run following command:

divine check --capture ./ --vfslimit 50M src/cmp README README

Divine segfaults even before DiOS starts to boot:

   $ divine check --capture ./ --vfslimit 50M src/cmp README README
   loading bitcode … DiOS … LART … RR … constants … Segmentation fault (core dumped)

Change History (0)

Note: See TracTickets for help on using tickets.