[ 0:00] compiling /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c [ 0:00] loading bitcode … LART … RR … constants … done [ 0:10] booting … done [ 0:12] [ 0:12] searching: 1 states found in 0:00, averaging 90.9, queued: 0 [ 0:13] found 13 states in 0:00, averaging 25.4 [ 0:13] [ 0:13] state count: 13 [ 0:13] states per second: 25.4403 [ 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: 1036468 [ 0:13] physical memory used: 466916 [ 0:13] user time: 6.710000 [ 0:13] system time: 0.250000 [ 0:13] wall time: 7.185450 [ 0:13] [ 0:15] timers: [ 0:15] lart: 1.07 [ 0:15] loader: 2.63 [ 0:15] boot: 1.74 [ 0:15] search: 0.511 [ 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.start-thread-a.c, line 23. [ 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* a2db8c69 0+0 [ 0:15] pc: code* 15b 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* 7bd0f0f5 0+0 [ 0:15] pc: code* 1b8 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* 8e736708 0+0 [ 0:15] pc: code* 1a0 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* 186 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* cf998ad8 0+0 [ 0:15] pc: code* 1011 15 [ 0:15] location: /divine/src/libc/functions/unistd/syscall.c:14 [ 0:15] symbol: __dios_trap [ 0:15] [ 0:15] - address: heap* 46d870b8 0+0 [ 0:15] pc: code* 1012 9 [ 0:15] location: /divine/src/libc/functions/unistd/syscall.c:26 [ 0:15] symbol: __dios_syscall [ 0:15] [ 0:15] - address: heap* 4a7d365c 0+0 [ 0:15] pc: code* 15a 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* c9c8eb5 0+0 [ 0:15] pc: code* 1008 11 [ 0:15] location: /divine/src/libc/functions/sys/fault.c:25 [ 0:15] symbol: __dios_fault [ 0:15] [ 0:15] - address: heap* e3f61522 0+0 [ 0:15] pc: code* 1003 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* 3 16 [ 0:15] location: /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c:23 [ 0:15] symbol: main [ 0:15] [ 0:15] - address: heap* 3340f329 0+0 [ 0:15] pc: code* 100f b [ 0:15] location: /divine/src/libc/functions/sys/start.cpp:72 [ 0:15] symbol: _start [ 0:15] [ 0:15] backtrace 3: [ 0:15] - address: heap* 275f634 0+0 [ 0:15] pc: code* 2 14 [ 0:15] location: /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c:15 [ 0:15] symbol: routine [ 0:15] [ 0:15] a report was written to verify.out [ 0:15] [ 0:22] ^ —————. —.— . . —.— . . .————— . . [ 0:22] ——— | | | | | | |\ | | | | [ 0:22] —(o)— | | | | | | | \ | |———— '————| [ 0:22] ——————— | | | \ / | | \| | | [ 0:22] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:22] [ 0:22] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:22] traced states: #1 #2 #3 #4 #5 [ 0:24] # executing void {Scheduler}::run_scheduler<{Context} >() [ 0:24] # at /divine/include/dios/core/scheduling.hpp:497 [ 0:24] T: (0) DiOS Fault: Assertion failed: 0, file /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c, line 23. [ 0:24] T: [0] Fault in userspace: diosassert [ 0:24] # executing {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:24] # at /divine/include/dios/core/fault.hpp:172 [ 0:24] - address: heap* a2db8c69 0+0 [ 0:24] pc: code* 15b 5c [ 0:24] location: /divine/include/dios/core/fault.hpp:172 [ 0:24] symbol: {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:24] [ 0:24] - address: heap* 7bd0f0f5 0+0 [ 0:24] pc: code* 1b8 e3 [ 0:24] location: /divine/include/dios/core/syscall.hpp:70 [ 0:24] symbol: {Syscall}::fault_handlerWrappper({Context}&, void*, __va_list_tag*) [ 0:24] [ 0:24] - address: heap* 8e736708 0+0 [ 0:24] pc: code* 1a0 14 [ 0:24] location: /divine/include/dios/core/syscall.hpp:41 [ 0:24] symbol: {Syscall}::handle({Context}&, _DiOS_Syscall&) [ 0:24] [ 0:24] - address: heap* 10 0+0 [ 0:24] pc: code* 186 41 [ 0:24] location: /divine/include/dios/core/scheduling.hpp:509 [ 0:24] symbol: void {Scheduler}::run_scheduler<{Context} >() [ 0:24] [ 0:24] backtrace 1: [ 0:24] - address: heap* cf998ad8 0+0 [ 0:24] pc: code* 1011 15 [ 0:24] location: /divine/src/libc/functions/unistd/syscall.c:14 [ 0:24] symbol: __dios_trap [ 0:24] [ 0:24] - address: heap* 46d870b8 0+0 [ 0:24] pc: code* 1012 9 [ 0:24] location: /divine/src/libc/functions/unistd/syscall.c:26 [ 0:24] symbol: __dios_syscall [ 0:24] [ 0:24] - address: heap* 4a7d365c 0+0 [ 0:24] pc: code* 15a 1c [ 0:24] location: /divine/include/dios/core/fault.hpp:198 [ 0:24] symbol: void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) [ 0:24] [ 0:24] - address: heap* c9c8eb5 0+0 [ 0:24] pc: code* 1008 11 [ 0:24] location: /divine/src/libc/functions/sys/fault.c:25 [ 0:24] symbol: __dios_fault [ 0:24] [ 0:24] - address: heap* e3f61522 0+0 [ 0:24] pc: code* 1003 2 [ 0:24] location: /divine/src/libc/functions/_PDCLIB/assert.c:21 [ 0:24] symbol: _PDCLIB_assert_dios [ 0:24] [ 0:24] - address: heap* fab409f3 0+0 [ 0:24] pc: code* 3 16 [ 0:24] location: /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c:23 [ 0:24] symbol: main [ 0:24] [ 0:24] - address: heap* 3340f329 0+0 [ 0:24] pc: code* 100f b [ 0:24] location: /divine/src/libc/functions/sys/start.cpp:72 [ 0:24] symbol: _start [ 0:24] [ 0:24] backtrace 2: [ 0:24] - address: heap* 275f634 0+0 [ 0:24] pc: code* 2 14 [ 0:24] location: /home/xrockai/src/divine/nightly/test/dios/api/2.start-thread-a.c:15 [ 0:24] symbol: routine [ 0:24] [ 0:24] # executing {Fault}::fault_handler(int, _VM_Frame*, int) [ 0:24] # at /divine/include/dios/core/fault.hpp:172