jan@jan-HP-ZBook-15u-G5:~$ spin -search mdev-23328.pl pan.c: In function ‘make_trail’: pan.c:2022:19: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=] 2022 | sprintf(fnm, "%s%d.%s", | ^~ pan.c:2022:16: note: directive argument in the range [1, 2147483647] 2022 | sprintf(fnm, "%s%d.%s", | ^~~~~~~~~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2030:22: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 2030 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2037:21: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=] 2037 | sprintf(fnm, "%s%d.%s", | ^~ pan.c:2037:18: note: directive argument in the range [1, 2147483646] 2037 | sprintf(fnm, "%s%d.%s", | ^~~~~~~~~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 523) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:2040:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 2040 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c: In function ‘findtrail’: pan.c:1626:22: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=] 1598 | tprefix = "trail"; | ~~~~~~~ ...... 1626 | { sprintf(fnm, "%s.%s", MyFile, tprefix); | ^~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1637:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 1637 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1602:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1602 | { sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1614:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1614 | sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1676:21: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=] 1663 | tprefix = "trail"; | ~~~~~~~ ...... 1676 | { sprintf(fnm, "%s.%s", MyFile, tprefix); | ^~ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 7 and 518 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1680:23: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=] 1680 | sprintf(fnm, "%s.%s", MyFile, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 2 or more bytes (assuming 513) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1666:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1666 | { sprintf(fnm, "%s%d.%s", MyFile, whichtrail, tprefix); | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output between 8 and 529 bytes into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pan.c:1670:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=] 1670 | sprintf(fnm, "%s%d.%s", | ^ In file included from /usr/include/stdio.h:867, from pan.c:7: /usr/include/x86_64-linux-gnu/bits/stdio2.h:36:10: note: ‘__builtin___sprintf_chk’ output 3 or more bytes (assuming 514) into a destination of size 512 36 | return __builtin___sprintf_chk (__s, __USE_FORTIFY_LEVEL - 1, | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 37 | __bos (__s), __fmt, __va_arg_pack ()); | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (Spin Version 6.4.9 -- 17 December 2018) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 44 byte, depth reached 32, errors: 0 268 states, stored 179 states, matched 447 transitions (= stored+matched) 24 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.018 equivalent memory usage for states (stored*(State-vector + overhead)) 0.286 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage unreached in proctype kill (0 of 25 states) unreached in proctype bf_kill (0 of 25 states) unreached in proctype monitor (0 of 5 states) unreached in init (0 of 5 states) pan: elapsed time 0 seconds