[ 0:00] + cat [ 0:00] + cat [ 0:00] + divcc -g -c f.c prog.c [ 0:00] prog.c:6:12: warning: implicit declaration of function 'f' is invalid in C99 [ 0:00] assert(f(i) != 7); /* ERROR */ [ 0:00] ^ [ 0:00] 1 warning generated. [ 0:00] + '[' -s f.o ']' [ 0:00] + '[' -s prog.o ']' [ 0:00] + ar cr f.a f.o [ 0:00] + '[' -s f.a ']' [ 0:01] + divcc prog.o f.a [ 0:01] + '[' -s linked.bc ']' [ 0:01] + '[' -s a.out ']' [ 0:01] + objdump -h a.out [ 0:01] + grep .llvmbc [ 0:01] 35 .llvmbc 00029da4 0000000000000000 0000000000000000 000034c9 2**0 [ 0:01] + divine verify a.out [ 0:01] + tee verify.out [ 0:01] states per second: 100 [ 0:03] state count: 2 [ 0:03] mips: 0.35 [ 0:03] [ 0:03] error found: yes [ 0:03] error trace: | [ 0:03] (0) Assertion failed: f(i) != 7, file prog.c, line 6. [ 0:03] [0] FATAL: assertion failure in userspace [ 0:03] [ 0:03] active stack: [ 0:03] a report was written to - symbol: void __dios::FaultBase::handler<__dios::Upcall<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::config::Base> > > > > >(_VM_Fault, _VM_Frame*, void (*)()) [ 0:03] location: /dios/include/dios/sys/fault.hpp:87 [ 0:03] - symbol: __dios_fault [ 0:03] location: /dios/src/libc/sys/fault.c:14 [ 0:03] - symbol: __assert_fail [ 0:03] location: /dios/src/libc/_PDCLIB/assert.c:21 [ 0:03] - symbol: main [ 0:03] location: prog.c:6 [ 0:03] - symbol: _start [ 0:03] location: /dios/src/libc/sys/start.cpp:102 [ 0:03] a.report [ 0:03] + check verify prog.c [ 0:03] + check debris