[ 0:00] | load /var/obj/divine-nightly/semidbg/test/_expand/dios/fairness.pkg.cpp/unfair.cpp unfair.cpp [ 0:00] | expect --result error --location unfair.cpp:37 [ 0:00] | cc -o testcase.bc -std=c++14 unfair.cpp [ 0:00] | verify --max-memory 4GiB --max-time 600 --threads 2 --report-filename verify.out --leakcheck exit --dios-config default --liveness -o nofail:malloc testcase.bc [ 0:00] compiling unfair.cpp [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:07] booting … done [ 0:07] states per second: 305.085 [ 0:07] state count: 18 [ 0:07] mips: 0.21 [ 0:07] [ 0:08] error found: yes [ 0:08] error trace: | [ 0:08] (0) Monitor registered [ 0:08] W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:08] W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:08] [ 0:08] stack 1: [ 0:08] - symbol: main [ 0:08] location: /dios/libcxx/include/atomic:957 [ 0:08] - symbol: __dios_start [ 0:08] location: /dios/libc/sys/start.cpp:94 [ 0:08] stack 2: [ 0:09] - symbol: main::$_0::operator()() const [ 0:09] location: unfair.cpp:70 [ 0:09] - symbol: void* std::__2::__thread_proxy >, main::$_0> >(void*) [ 0:09] location: /dios/libcxx/include/type_traits:3530 [ 0:09] - symbol: __pthread_start [ 0:09] location: /dios/libc/pthread/pthread-init.cpp:79 [ 0:09] - symbol: __pthread_entry [ 0:09] location: /dios/libc/pthread/pthread-core.cpp:50 [ 0:09] active stack: [ 0:09] - symbol: __buchi_accept() [ 0:10] location: unfair.cpp:54 [ 0:10] - symbol: BuchiAutomaton::step() [ 0:10] location: unfair.cpp:37 [ 0:10] - symbol: __dios::MonitorManager<__dios::BaseContext>::runMonitors() [ 0:10] location: /dios/include/sys/monitor.h:33 [ 0:10] - symbol: void __dios::Scheduler<__dios::Clock<__dios::NondetChoose<__dios::Base> > >::run_scheduler<__dios::Context>() [ 0:10] location: /dios/sys/sched_base.hpp:442 [ 0:10] + divine sim --batch --skip-init --load-report verify.out [ 0:10] [ 0:15] ^ —————. —.— . . —.— . . .————— . . [ 0:15] ——— | | | | | | |\ | | | | [ 0:15] —(o)— | | | | | | | \ | |———— '————| [ 0:15] ——————— | | | \ / | | \| | | [ 0:15] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:15] [ 0:15] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:15] traced states: [ 0:16] trace: [ 0:16] T: (0) Monitor registered [ 0:16] T: W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* 65fbc4d5 0 ddp] and [heap* ce719923 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:16] T: W: pointer-dependent operation with [heap* ce719923 0 ddp] and [heap* 65fbc4d5 0 ddp] in debug mode (abandoned) [ 0:16] ▶ state #11 [new] -- active threads: [0:0] 0:1 -- [ 0:16] # executing __buchi_accept() at unfair.cpp:55 [ 0:16] # NOTE: $frame in BuchiAutomaton::step() [ 0:16] > backtrace [ 0:16] __buchi_accept() at unfair.cpp:55 [ 0:16] BuchiAutomaton::step() at unfair.cpp:37 [ 0:16] {Monitor}::runMonitors() at /dios/include/sys/monitor.h:33 [ 0:16] void {Scheduler}::run_scheduler<{Context}>() at /dios/sys/sched_base.hpp:442 [ 0:16] # backtrace 1: [ 0:16] main at /dios/libcxx/include/atomic:957 [ 0:16] __dios_start at /dios/libc/sys/start.cpp:94 [ 0:16] # backtrace 2: [ 0:16] main::$_0::operator()() const at unfair.cpp:70 [ 0:16] void* std::__2::__thread_proxy >, main::$_0> >(void*) at /dios/libcxx/include/type_traits:3530 [ 0:16] __pthread_start at /dios/libc/pthread/pthread-init.cpp:79 [ 0:16] __pthread_entry at /dios/libc/pthread/pthread-core.cpp:50 [ 0:16] # executing __buchi_accept() at unfair.cpp:55 [ 0:17] # NOTE: $frame in BuchiAutomaton::step()