[ 0:00] + sim /home/xrockai/src/divine/nightly/test/c/1.malloc.c [ 0:00] compiling /home/xrockai/src/divine/nightly/test/c/1.malloc.c [ 0:00] [ 0:10] ^ —————. —.— . . —.— . . .————— . . [ 0:10] ——— | | | | | | |\ | | | | [ 0:10] —(o)— | | | | | | | \ | |———— '————| [ 0:10] ——————— | | | \ / | | \| | | [ 0:10] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:10] [ 0:10] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:10] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:10] > setup --debug libc [ 0:10] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:10] > trace --choices 0 0 1 [ 0:10] traced states: #1 #2 [ 0:15] # executing malloc at /divine/src/libc/functions/_PDCLIB/glue.c:31 [ 0:15] > stepa --count 3 [ 0:15] # a new program state was stored as #3 [ 0:15] # active threads: [0:0] [ 0:15] # a new program state was stored as #4 [ 0:17] # executing - at - [ 0:17] > trace --choices 0 0 0 [ 0:17] traced states: #1 #2 [ 0:21] # executing malloc at /divine/src/libc/functions/_PDCLIB/glue.c:31 [ 0:21] > step --out [ 0:21] %10 = icmp.eq %0f [i32 0 d] # [i1 1 1] [ 0:21] br %10 label %if.then label %if.end [ 0:21] %19 = and %07 [i64 1 d] # [i64 0 d] [ 0:21] %1a = vm.control [i32 1 d] [i32 7 d] [i32 2 d] [i32 7 d] # [global* 0 1 ddn] [ 0:21] [i64 1 d] %19 [code* 0 0 ddp] [ 0:21] ret %18 [ 0:21] # executing main at /home/xrockai/src/divine/nightly/test/c/1.malloc.c:6 [ 0:21] > step --count 2 [ 0:21] store [i32 32 d] %03 [ 0:21] T: FAULT: null pointer dereference: [global* 0 0 ddp] [ 0:21] %05 = alloca [i32 1 d] # [heap* a33a7c28 0 ddp] [ 0:21] # executing __dios_syscall at /divine/src/libc/functions/unistd/syscall.c:22 [ 0:21] > trace --choices 0 0 0 0 [ 0:21] traced states: #1 #2 #4 [ 0:26] unused choices: 0/0 [ 0:26] trace: [ 0:26] T: FAULT: null pointer dereference: [global* 0 0 ddp] [ 0:26] T: [0] FATAL: memory error in userspace [ 0:26] ERROR: the program has already terminated [ 0:26] # executing - at - [ 0:26] [ 0:27] = expected ========== [ 0:27] + ^# executing __boot at [ 0:27] > setup --debug libc [ 0:27] > trace --choices 0 0 1 [ 0:27] - FAULT [ 0:27] + ^traced states: #1 #2 [ 0:27] + ^# executing malloc at [ 0:27] > stepa --count 3 [ 0:27] + ^# executing - at - [ 0:27] > trace --choices 0 0 0 [ 0:27] + ^traced states: #1 #2 [ 0:27] + ^# executing malloc at [ 0:27] > step --out [ 0:27] > step --count 2 [ 0:27] + ^T: FAULT: null pointer dereference [ 0:27] + ^# executing __dios_syscall [ 0:27] > trace --choices 0 0 0 0 [ 0:27] + traced states: #1 #2 #4 [ 0:27] + unused choices: 0/0 [ 0:27] [ 0:27] = matched =========== [ 0:27] # executing __boot at /divine/src/dios/core/dios.cpp:169 | ^# executing __boot at [ 0:27] > setup --debug libc | ^> setup --debug libc [ 0:27] > trace --choices 0 0 1 | ^> trace --choices 0 0 1 [ 0:27] traced states: #1 #2 | ^traced states: #1 #2 [ 0:27] # executing malloc at /divine/src/libc/functions/_PDCLIB/glue.c:31 | ^# executing malloc at [ 0:27] > stepa --count 3 | ^> stepa --count 3 [ 0:27] # executing - at - | ^# executing - at - [ 0:27] > trace --choices 0 0 0 | ^> trace --choices 0 0 0 [ 0:27] traced states: #1 #2 | ^traced states: #1 #2 [ 0:27] # executing malloc at /divine/src/libc/functions/_PDCLIB/glue.c:31 | ^# executing malloc at [ 0:27] > step --out | ^> step --out [ 0:27] > step --count 2 | ^> step --count 2 [ 0:27] T: FAULT: null pointer dereference: [global* 0 0 ddp] | ^T: FAULT: null pointer dereference [ 0:27] # executing __dios_syscall at /divine/src/libc/functions/unistd/syscall.c:22 | ^# executing __dios_syscall [ 0:27] > trace --choices 0 0 0 0 | ^> trace --choices 0 0 0 0 [ 0:27] traced states: #1 #2 #4 | traced states: #1 #2 #4 [ 0:27] unused choices: 0/0 | unused choices: 0/0 [ 0:27] + tee loop.c [ 0:27] #include [ 0:27] [ 0:27] void __sched() {} [ 0:27] int main() {} [ 0:27] [ 0:27] void __boot() [ 0:27] { [ 0:27] __vm_control( _VM_CA_Set, _VM_CR_State, __vm_obj_make( 4 ) ); [ 0:27] __vm_control( _VM_CA_Set, _VM_CR_Scheduler, __sched ); [ 0:27] } [ 0:27] + sim loop.c [ 0:27] compiling loop.c [ 0:27] [ 0:38] ^ —————. —.— . . —.— . . .————— . . [ 0:38] ——— | | | | | | |\ | | | | [ 0:38] —(o)— | | | | | | | \ | |———— '————| [ 0:38] ——————— | | | \ / | | \| | | [ 0:38] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:38] [ 0:38] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:38] # executing __boot at loop.c:8 [ 0:38] > trace --choices 0 0 [ 0:38] traced states: #1 #1 [loop closed] [ 0:40] unused choices: 0/0 0/0 [ 0:40] ERROR: could not reach userspace [ 0:40] # executing - at - [ 0:40] [ 0:42] = expected ========== [ 0:42] > trace --choices 0 0 [ 0:42] + traced states: #1 #1 \[loop closed\] [ 0:42] + unused choices: 0/0 0/0 [ 0:42] [ 0:42] = matched =========== [ 0:42] > trace --choices 0 0 | ^> trace --choices 0 0 [ 0:42] traced states: #1 #1 [loop closed] | traced states: #1 #1 \[loop closed\] [ 0:42] unused choices: 0/0 0/0 | unused choices: 0/0 0/0 [ 0:42] + check debris