Opened 4 years ago

Closed 3 years ago

#110 closed defect (fixed)

DiOS: -o {stdout|stderr}:notrace results in a null pointer dereference

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


it is not possible to disable DiOS' stderr and stdout tracing in Divine's reports at the moment. Sometimes it's not quite clear which lines of the error trace were from DiOS and which from the io of the verified code as we are automatically processing the reports.

$ divine check -o stdout:notrace divine-stdout.c
compiling divine-stdout.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 0
state count: 0
mips: 0

error found: boot
error trace: |
  FAULT: null pointer dereference: [global* 0 8 ddn]
  DOUBLE FAULT: trying to return without a caller

a report was written to

Change History (2)

comment:1 Changed 4 years ago by Lukáš Zaoral

Component: otherDiOS

comment:2 Changed 3 years ago by mornfall

Resolution: fixed
Status: newclosed

Fixed in next.

Note: See TracTickets for help on using tickets.