[ 0:00] + cat [ 0:00] + dioscc -o gnu -D_GNU_SOURCE strerr_gnu.c [ 0:00] strerr_gnu.c:8:5: warning: implicitly declaring library function 'printf' with type 'int (const char *, ...)' [ 0:00] printf( "%s\n", ret ); [ 0:00] ^ [ 0:00] strerr_gnu.c:8:5: note: include the header or explicitly provide a declaration for 'printf' [ 0:00] 1 warning generated. [ 0:00] + '[' -s a.out ']' [ 0:00] + '[' -s gnu ']' [ 0:00] + '[' -x gnu ']' [ 0:00] + ./gnu [ 0:00] No such process [ 0:00] + echo 'expect --result valid' [ 0:00] + echo 'check gnu' [ 0:00] + divcheck script [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:02] booting … done [ 0:03] states per second: 225.806 [ 0:03] state count: 14 [ 0:03] mips: 0.15 [ 0:03] error found: no [ 0:03] + divine exec --virtual gnu [ 0:03] + fgrep 'o such process' [ 0:03] loading bitcode … DiOS … LART … RR … constants … done [ 0:05] booting … done [ 0:05] a report was written to gnu.report [ 0:06] [0] ESRCH (no such process) [ 0:06] + cat [ 0:06] + dioscc -o nognu -D_XOPEN_SOURCE strerr_nognu.c [ 0:06] strerr_nognu.c:8:5: warning: implicitly declaring library function 'printf' with type 'int (const char *, ...)' [ 0:06] printf( "%s\n", buf ); [ 0:06] ^ [ 0:06] strerr_nognu.c:8:5: note: include the header or explicitly provide a declaration for 'printf' [ 0:06] 1 warning generated. [ 0:06] + '[' -s a.out ']' [ 0:07] + '[' -s nognu ']' [ 0:07] + '[' -x nognu ']' [ 0:07] + ./nognu [ 0:07] No such process [ 0:07] + echo 'expect --result valid' [ 0:07] + echo 'check nognu' [ 0:07] + divcheck script [ 0:07] loading bitcode … DiOS … LART … RR … constants … done [ 0:09] booting … done [ 0:09] states per second: 237.288 [ 0:09] state count: 14 [ 0:09] mips: 0.16 [ 0:09] error found: no [ 0:09] + divine exec --virtual nognu [ 0:09] + fgrep 'o such process' [ 0:09] loading bitcode … DiOS … LART … RR … constants … done [ 0:12] booting … done [ 0:12] a report was written to nognu.report [ 0:12] [0] ESRCH (no such process) [ 0:13] + check debris [ 0:13] + test -e warning