#110 new defect

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 (1)

comment:1 Changed 5 months ago by Lukáš Zaoral

Component:	other → DiOS

Note: See TracTickets for help on using tickets.