Opened 5 years ago

Closed 4 years ago

#97 closed defect (fixed)

DiOS: Passing the debug:mainargs option results in config error in kernel

Reported by: Lukáš Zaoral Owned by: Vladimír Štill
Priority: major Milestone: 4.4
Component: DiOS Keywords:
Cc: kdudka@…, jamartis@…, lzaoral@…

Description

Hello,
running divine check with the -o debug:mainargs` option results in a config error in DiOS's kernel. Thanks.

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

  error found: boot
  error trace: |
    [  ] ERROR: Unused option debug:mainargs
    FAULT: Unused options
    [  ] FATAL: config error in kernel
    have_debug() failed in debug mode
    W: debug mode cannot be changed in debug mode (abandoned)
    have_debug() failed in debug mode
    W: debug mode cannot be changed in debug mode (abandoned)
  boot info:
    main argv:
      0: main.c
    main envp:


  a report was written to main.report

Attachments (1)

main.report​ (5.1 KB) - added by Lukáš Zaoral 5 years ago.

Download all attachments as: .zip

Change History (3)

Changed 5 years ago by Lukáš Zaoral

Attachment: main.report​ added

comment:1 Changed 5 years ago by Vladimír Štill

Owner: set to Vladimír Štill
Status: new → accepted

comment:2 Changed 4 years ago by mornfall

Resolution: → fixed
Status: accepted → closed

Fixed in next.

Note: See TracTickets for help on using tickets.