[ 0:00] /home/xrockai/src/divine/nightly/test/lib/pdclib-test: line 1: lib/flavour: No such file or directory [ 0:00] + EXTRA_FILES= [ 0:00] + FLAGS= [ 0:00] + . /home/xrockai/src/divine/nightly/test/pdclib/_PDCLIB-_PDCLIB_latin1.pdc [ 0:00] ++ TESTCASE=_PDCLIB/_PDCLIB_latin1.c [ 0:00] + test -n _PDCLIB/_PDCLIB_latin1.c [ 0:00] + FILE=/home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c [ 0:00] + test -f /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c [ 0:00] + grep -w NO_TESTDRIVER /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c [ 0:00] + divine cc -D_PDCLIB_BUILD -DTEST -I/home/xrockai/src/divine/nightly/dios/libc/testing /home/xrockai/src/divine/nightly/test/pdclib/testenv.helper.c /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c -o unittest.bc [ 0:00] compiling /home/xrockai/src/divine/nightly/test/pdclib/testenv.helper.c [ 0:00] compiling /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:88:44: warning: passing 'char **' to parameter of type 'const char *restrict *' discards qualifiers in nested pointer types [ 0:00] TESTCASE(latin1toc32(&c32ptr, &c32rem, &chrptr, &chrrem, &mbs) == true); [ 0:00] ^~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/testing/_PDCLIB_test.h:36:28: note: expanded from macro 'TESTCASE' [ 0:00] #define TESTCASE( x ) if ( x ) {} \ [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:18:42: note: passing argument to parameter 'p_inbuf' here [ 0:00] const char *restrict *restrict p_inbuf, [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:103:44: warning: passing 'char32_t **' (aka 'unsigned int **') to parameter of type 'const char32_t *restrict *' (aka 'const unsigned int *restrict *') discards qualifiers in nested pointer types [ 0:00] TESTCASE(c32tolatin1(&chrptr, &chrrem, &c32ptr, &c32rem, &mbs) == true); [ 0:00] ^~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/testing/_PDCLIB_test.h:36:28: note: expanded from macro 'TESTCASE' [ 0:00] #define TESTCASE( x ) if ( x ) {} \ [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:41:41: note: passing argument to parameter 'p_inbuf' here [ 0:00] const char32_t *restrict *restrict p_inbuf, [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:116:44: warning: passing 'char32_t **' (aka 'unsigned int **') to parameter of type 'const char32_t *restrict *' (aka 'const unsigned int *restrict *') discards qualifiers in nested pointer types [ 0:00] TESTCASE(c32tolatin1(&chrptr, &chrrem, &c32ptr, &c32rem, &mbs) == false); [ 0:00] ^~~~~~~ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/testing/_PDCLIB_test.h:36:28: note: expanded from macro 'TESTCASE' [ 0:00] #define TESTCASE( x ) if ( x ) {} \ [ 0:00] ^ [ 0:00] /home/xrockai/src/divine/nightly/dios/libc/_PDCLIB/_PDCLIB_latin1.c:41:41: note: passing argument to parameter 'p_inbuf' here [ 0:00] const char32_t *restrict *restrict p_inbuf, [ 0:00] ^ [ 0:00] 3 warnings generated. [ 0:00] + llvm-nm unittest.bc [ 0:00] + grep -w 'T main' [ 0:00] ---------------- T main [ 0:00] + divine verify --max-memory 4GiB --threads 1 -o nofail:malloc unittest.bc [ 0:00] + tee verify.out [ 0:00] loading bitcode … DiOS … LART … RR … constants … done [ 0:03] booting … done [ 0:03] states per second: 191.489 [ 0:03] state count: 9 [ 0:03] mips: 0.21 [ 0:03] error found: no [ 0:03] a report was written to unittest.report [ 0:03] + check verify /home/xrockai/src/divine/nightly/test/pdclib/_PDCLIB-_PDCLIB_latin1.pdc [ 0:04] + check debris [ 0:04] + test -e warning