[ 0:01] compiling /home/xrockai/src/divine/nightly/test/dios/api/2.kill-thread-a.c [ 0:01] loading bitcode … LART … RR … constants … done [ 0:11] booting … done [ 0:12] [ 0:12] searching: 1 states found in 0:00, averaging 83.3, queued: 0 [ 0:13] found 15 states in 0:00, averaging 29.2 [ 0:13] [ 0:13] state count: 15 [ 0:13] states per second: 29.2398 [ 0:13] version: 4.0.15+10085445e9eb [ 0:13] [ 0:13] architecture: Intel(R) Xeon(R) CPU E5-2630 v2 @ 2.60GHz [ 0:13] memory used: 1036476 [ 0:13] physical memory used: 465188 [ 0:13] user time: 6.760000 [ 0:13] system time: 0.210000 [ 0:13] wall time: 7.143805 [ 0:13] [ 0:15] timers: [ 0:15] lart: 1.05 [ 0:15] loader: 2.6 [ 0:15] boot: 1.73 [ 0:15] search: 0.513 [ 0:15] ce: 1.98 [ 0:15] error found: yes [ 0:15] error trace: | [ 0:15] (0) DiOS Fault: Assertion failed: 0, file /home/xrockai/src/divine/nightly/test/dios/api/2.kill-thread-a.c, line 18. [ 0:15] [0] Fault in userspace: diosassert [ 0:15] [0] Backtrace: [ 0:15] [0] 1: __dios_fault [ 0:15] [0] 2: _PDCLIB_assert_dios [ 0:15] [0] 3: main [ 0:15] [0] 4: _start [ 0:15] [ 0:15] error state: [ 0:15] backtrace 1: # active stack [ 0:15] - address: heap* 14ddd833 0+0 [ 0:15] pc: code* 159 5c [ 0:15] location: /divine/include/dios/core/fault.hpp:172 [ 0:15] symbol: {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:15] [ 0:15] - address: heap* e801adce 0+0 [ 0:15] pc: code* 1b6 e3 [ 0:15] location: /divine/include/dios/core/syscall.hpp:70 [ 0:15] symbol: {Syscall}::fault_handlerWrappper({Context}&, void*, __va_list_tag*) [ 0:15] [ 0:15] - address: heap* d1503e01 0+0 [ 0:15] pc: code* 19e 14 [ 0:15] location: /divine/include/dios/core/syscall.hpp:41 [ 0:15] symbol: {Syscall}::handle({Context}&, _DiOS_Syscall&) [ 0:15] [ 0:15] - address: heap* 10 0+0 [ 0:15] pc: code* 184 41 [ 0:15] location: /divine/include/dios/core/scheduling.hpp:509 [ 0:15] symbol: void {Scheduler}::run_scheduler<{Context} >() [ 0:15] [ 0:15] backtrace 2: [ 0:15] - address: heap* 29abbc9a 0+0 [ 0:15] pc: code* 100f 15 [ 0:15] location: /divine/src/libc/functions/unistd/syscall.c:14 [ 0:15] symbol: __dios_trap [ 0:15] [ 0:15] - address: heap* 2c4daf7f 0+0 [ 0:15] pc: code* 1010 9 [ 0:15] location: /divine/src/libc/functions/unistd/syscall.c:26 [ 0:15] symbol: __dios_syscall [ 0:15] [ 0:15] - address: heap* c390dd70 0+0 [ 0:15] pc: code* 158 1c [ 0:15] location: /divine/include/dios/core/fault.hpp:198 [ 0:15] symbol: void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) [ 0:15] [ 0:15] - address: heap* f98a3b86 0+0 [ 0:15] pc: code* 1006 11 [ 0:15] location: /divine/src/libc/functions/sys/fault.c:25 [ 0:15] symbol: __dios_fault [ 0:15] [ 0:15] - address: heap* a0aceb6e 0+0 [ 0:15] pc: code* 1001 2 [ 0:15] location: /divine/src/libc/functions/_PDCLIB/assert.c:21 [ 0:15] symbol: _PDCLIB_assert_dios [ 0:15] [ 0:15] - address: heap* fab409f3 0+0 [ 0:15] pc: code* 2 1b [ 0:15] location: /home/xrockai/src/divine/nightly/test/dios/api/2.kill-thread-a.c:18 [ 0:15] symbol: main [ 0:15] [ 0:15] - address: heap* 3340f329 0+0 [ 0:15] pc: code* 100d b [ 0:15] location: /divine/src/libc/functions/sys/start.cpp:72 [ 0:15] symbol: _start [ 0:15] [ 0:15] a report was written to verify.out [ 0:15] [ 0:23] ^ —————. —.— . . —.— . . .————— . . [ 0:23] ——— | | | | | | |\ | | | | [ 0:23] —(o)— | | | | | | | \ | |———— '————| [ 0:23] ——————— | | | \ / | | \| | | [ 0:23] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:23] [ 0:23] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:23] traced states: #1 #2 #3 #4 #5 #6 #7 [ 0:25] # executing void {Scheduler}::run_scheduler<{Context} >() [ 0:25] # at /divine/include/dios/core/scheduling.hpp:497 [ 0:25] T: (0) DiOS Fault: Assertion failed: 0, file /home/xrockai/src/divine/nightly/test/dios/api/2.kill-thread-a.c, line 18. [ 0:25] T: [0] Fault in userspace: diosassert [ 0:25] # executing {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:25] # at /divine/include/dios/core/fault.hpp:172 [ 0:25] - address: heap* 14ddd833 0+0 [ 0:25] pc: code* 159 5c [ 0:25] location: /divine/include/dios/core/fault.hpp:172 [ 0:25] symbol: {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:25] [ 0:25] - address: heap* e801adce 0+0 [ 0:25] pc: code* 1b6 e3 [ 0:25] location: /divine/include/dios/core/syscall.hpp:70 [ 0:25] symbol: {Syscall}::fault_handlerWrappper({Context}&, void*, __va_list_tag*) [ 0:25] [ 0:25] - address: heap* d1503e01 0+0 [ 0:25] pc: code* 19e 14 [ 0:25] location: /divine/include/dios/core/syscall.hpp:41 [ 0:25] symbol: {Syscall}::handle({Context}&, _DiOS_Syscall&) [ 0:25] [ 0:25] - address: heap* 10 0+0 [ 0:25] pc: code* 184 41 [ 0:25] location: /divine/include/dios/core/scheduling.hpp:509 [ 0:25] symbol: void {Scheduler}::run_scheduler<{Context} >() [ 0:25] [ 0:25] backtrace 1: [ 0:25] - address: heap* 29abbc9a 0+0 [ 0:25] pc: code* 100f 15 [ 0:25] location: /divine/src/libc/functions/unistd/syscall.c:14 [ 0:25] symbol: __dios_trap [ 0:25] [ 0:25] - address: heap* 2c4daf7f 0+0 [ 0:25] pc: code* 1010 9 [ 0:25] location: /divine/src/libc/functions/unistd/syscall.c:26 [ 0:25] symbol: __dios_syscall [ 0:25] [ 0:25] - address: heap* c390dd70 0+0 [ 0:25] pc: code* 158 1c [ 0:25] location: /divine/include/dios/core/fault.hpp:198 [ 0:25] symbol: void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) [ 0:25] [ 0:25] - address: heap* f98a3b86 0+0 [ 0:25] pc: code* 1006 11 [ 0:25] location: /divine/src/libc/functions/sys/fault.c:25 [ 0:25] symbol: __dios_fault [ 0:25] [ 0:25] - address: heap* a0aceb6e 0+0 [ 0:25] pc: code* 1001 2 [ 0:25] location: /divine/src/libc/functions/_PDCLIB/assert.c:21 [ 0:25] symbol: _PDCLIB_assert_dios [ 0:25] [ 0:25] - address: heap* fab409f3 0+0 [ 0:25] pc: code* 2 1b [ 0:25] location: /home/xrockai/src/divine/nightly/test/dios/api/2.kill-thread-a.c:18 [ 0:25] symbol: main [ 0:25] [ 0:25] - address: heap* 3340f329 0+0 [ 0:25] pc: code* 100d b [ 0:25] location: /divine/src/libc/functions/sys/start.cpp:72 [ 0:25] symbol: _start [ 0:25] [ 0:25] # executing {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:25] # at /divine/include/dios/core/fault.hpp:172