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@…

Description

Hi,
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.
Thanks!

$ 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 divine-stdout.report

Change History (2)

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

Component: other → DiOS

comment:2 Changed 3 years ago by mornfall

Resolution: → fixed
Status: new → closed

Fixed in next.

Note: See TracTickets for help on using tickets.