[ 0:00] + cat
[ 0:00] + cat
[ 0:00] + dioscc -c foo.c
[ 0:00] + ar r libfoo.a foo.o
[ 0:00] ar: creating libfoo.a
[ 0:00] + nm libfoo.a
[ 0:00] + grep 'T foo'
[ 0:00] 0000000000000000 T foo
[ 0:00] + cat
[ 0:00] + dioscc main.c libfoo.a
[ 0:00] + ./a.out
[ 0:00] + divine check a.out
[ 0:00] loading bitcode … DiOS … LART … RR … constants … done
[ 0:03] booting … done
[ 0:04] states per second: 76.9231
[ 0:04] state count: 3
[ 0:04] mips: 0.16
[ 0:04] error found: no
[ 0:04] a report was written to a.report
[ 0:04] + rm a.out
[ 0:04] + dioscc main.c -L. -lfoo
[ 0:04] + ./a.out
[ 0:04] + divine check a.out
[ 0:04] loading bitcode … DiOS … LART … RR … constants … done
[ 0:06] booting … done
[ 0:06] states per second: 93.75
[ 0:07] state count: 3
[ 0:07] mips: 0.2
[ 0:07] error found: no
[ 0:07] a report was written to a.report
[ 0:07] + check debris
[ 0:07] + test -e warning