[ 0:01] + cat
[ 0:01] + dioscc -o gnu -D_GNU_SOURCE strerr_gnu.c
[ 0:01] strerr_gnu.c:8:5: warning: implicitly declaring library function 'printf' with type 'int (const char *, ...)'
[ 0:01]     printf( "%s\n", ret );
[ 0:01]     ^
[ 0:01] strerr_gnu.c:8:5: note: include the header <stdio.h> or explicitly provide a declaration for 'printf'
[ 0:01] 1 warning generated.
[ 0:01] + '[' -s a.out ']'
[ 0:01] + '[' -s gnu ']'
[ 0:01] + '[' -x gnu ']'
[ 0:01] + ./gnu
[ 0:01] No such process
[ 0:01] + echo 'expect --result valid'
[ 0:01] + echo 'check gnu'
[ 0:01] + divcheck script
[ 0:01] loading bitcode … DiOS … LART … RR … constants … done
[ 0:03] booting … done
[ 0:03] states per second: 444.444
[ 0:03] state count: 20
[ 0:03] mips: 0.21
[ 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:05] [0] ESRCH (no such process)
[ 0:05] + cat
[ 0:05] + dioscc -o nognu -D_XOPEN_SOURCE strerr_nognu.c
[ 0:05] 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 <stdio.h> or explicitly provide a declaration for 'printf'
[ 0:06] 1 warning generated.
[ 0:06] + '[' -s a.out ']'
[ 0:06] + '[' -s nognu ']'
[ 0:06] + '[' -x nognu ']'
[ 0:06] + ./nognu
[ 0:06] No such process
[ 0:06] + echo 'expect --result valid'
[ 0:06] + echo 'check nognu'
[ 0:06] + divcheck script
[ 0:06] loading bitcode … DiOS … LART … RR … constants … done
[ 0:08] booting … done
[ 0:08] states per second: 312.5
[ 0:08] state count: 20
[ 0:08] mips: 0.15
[ 0:08] error found: no
[ 0:08] + divine exec --virtual nognu
[ 0:08] + fgrep 'o such process'
[ 0:08] loading bitcode … DiOS … LART … RR … constants … done
[ 0:10] booting … done
[ 0:10] a report was written to nognu.report
[ 0:10] [0] ESRCH (no such process)
[ 0:10] + check debris
[ 0:10] + test -e warning