[ 0:01] + sim /home/xrockai/src/divine/nightly/test/c/1.assert.c [ 0:01] compiling /home/xrockai/src/divine/nightly/test/c/1.assert.c [ 0:01] [ 0:11] ^ —————. —.— . . —.— . . .————— . . [ 0:11] ——— | | | | | | |\ | | | | [ 0:11] —(o)— | | | | | | | \ | |———— '————| [ 0:11] ——————— | | | \ / | | \| | | [ 0:11] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:11] [ 0:11] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:11] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:11] > setup --sticky "source" [ 0:11] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:11] > setup --sticky "backtrace" [ 0:11] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:11] > start [ 0:11] # a new program state was stored as #1 [ 0:14] # active threads: [0:0] [ 0:14] # a new program state was stored as #2 [ 0:15] # active threads: [0:0] [ 0:15] 3 int main() [ 0:15] 4 { [ 0:15] >> 5 assert( 0 ); /* ERROR */ [ 0:15] 6 return 0; [ 0:15] 7 } [ 0:15] main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 [ 0:15] _start at /divine/src/libc/functions/sys/start.cpp:76 [ 0:15] # executing main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 [ 0:15] [ 0:16] = expected ========== [ 0:16] + ^# executing __boot at [ 0:16] > setup --sticky "source" [ 0:16] > setup --sticky "backtrace" [ 0:16] > start [ 0:16] + ^\s*3 int main\(\) [ 0:16] + main at [ 0:16] + _start at [ 0:16] [ 0:16] = matched =========== [ 0:16] # executing __boot at /divine/src/dios/core/dios.cpp:169 | ^# executing __boot at [ 0:16] > setup --sticky "source" | ^> setup --sticky "source" [ 0:16] > setup --sticky "backtrace" | ^> setup --sticky "backtrace" [ 0:16] > start | ^> start [ 0:16] 3 int main() | ^\s*3 int main\(\) [ 0:16] main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 | main at [ 0:16] _start at /divine/src/libc/functions/sys/start.cpp:76 | _start at [ 0:16] + sim /home/xrockai/src/divine/nightly/test/c/1.assert.c [ 0:16] compiling /home/xrockai/src/divine/nightly/test/c/1.assert.c [ 0:16] [ 0:27] ^ —————. —.— . . —.— . . .————— . . [ 0:27] ——— | | | | | | |\ | | | | [ 0:27] —(o)— | | | | | | | \ | |———— '————| [ 0:27] ——————— | | | \ / | | \| | | [ 0:27] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:27] [ 0:27] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:27] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:27] > start [ 0:27] # a new program state was stored as #1 [ 0:30] # active threads: [0:0] [ 0:30] # a new program state was stored as #2 [ 0:31] # active threads: [0:0] [ 0:31] # executing main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 [ 0:31] > setup --sticky "backtrace " [ 0:31] # executing main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 [ 0:31] > stepa [ 0:31] T: (0) FAULT: Assertion failed: 0, file /home/xrockai/src/divine/nightly/test/c/1.assert.c, line 5. [ 0:31] T: [0] FATAL: assertion failure in userspace [ 0:31] void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) at /divine/include/dios/core/fault.hpp:187 [ 0:31] __dios_fault at /divine/src/libc/functions/sys/fault.c:25 [ 0:31] main at /home/xrockai/src/divine/nightly/test/c/1.assert.c:5 [ 0:31] _start at /divine/src/libc/functions/sys/start.cpp:76 [ 0:31] # executing void {Fault}::handler<{Context} >(_VM_Fault, _VM_Frame*, void (*)(), ...) at /divine/include/dios/core/fault.hpp:187 [ 0:31] [ 0:33] = expected ========== [ 0:33] + ^# executing __boot at [ 0:33] > start [ 0:33] > setup --sticky "backtrace " [ 0:33] > stepa [ 0:33] [ 0:33] = matched =========== [ 0:33] # executing __boot at /divine/src/dios/core/dios.cpp:169 | ^# executing __boot at [ 0:33] > start | ^> start [ 0:33] > setup --sticky "backtrace " | ^> setup --sticky "backtrace " [ 0:33] > stepa | ^> stepa [ 0:33] + check debris