Excessive warnings thrown for `spin -run`

Maxvonhippel · 2020-07-30 19:00:38

When I run `spin` on a fairly simple model, I get tons of warnings:

````
pan.c: In function ‘make_trail’:
pan.c:2172:19: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
2172 | sprintf(fnm, "%s%d.%s",
| ^~
pan.c:2172:16: note: directive argument in the range [1, 2147483647]
2172 | 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:2180:22: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
2180 | 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:2187:21: warning: ‘%d’ directive writing between 1 and 10 bytes into a region of size between 1 and 512 [-Wformat-overflow=]
2187 | sprintf(fnm, "%s%d.%s",
| ^~
pan.c:2187:18: note: directive argument in the range [1, 2147483646]
2187 | 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:2190:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
2190 | 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:1776:22: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
1748 | tprefix = "trail";
| ~~~~~~~
......
1776 | { 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:1787:24: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
1787 | 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:1752:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1752 | { 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:1764:23: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1764 | 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:1826:21: warning: ‘%s’ directive writing 5 bytes into a region of size between 0 and 511 [-Wformat-overflow=]
1813 | tprefix = "trail";
| ~~~~~~~
......
1826 | { 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:1830:23: warning: ‘__builtin___sprintf_chk’ may write a terminating nul past the end of the destination [-Wformat-overflow=]
1830 | 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:1816:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1816 | { 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:1820:22: warning: ‘.’ directive writing 1 byte into a region of size between 0 and 511 [-Wformat-overflow=]
1820 | 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:1: invalid end state (at depth 2)
pan: wrote abs.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +

State-vector 148 byte, depth reached 3, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.001 equivalent memory usage for states (stored*(State-vector + overhead))
0.279 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

pan: elapsed time 0 seconds
````

Is there a way to make Spin not throw so many warnings? I am on Linux Mint 20, on a 2018 XPS 13. Thanks!

spinroot · 2020-07-31 21:49:55

ouch, those are new warnings that gcc generates based on more aggressive static analysis.
you could try passing the -Wformat-overflow=0 flag to the gcc call in the Spin sources, which
will suppress these warnings until more of them have been fixed.

spinroot · 2020-07-31 23:05:08

I've updated the Spin sources on Github (specifically main.c and version.h) to fix this.

Maxvonhippel · 2020-08-01 04:14:01

Thank you Gerard, I appreciate it! I made a tool that uses Spin as a back-end, and these warnings can be troublesome

Spinroot

#1 2020-07-30 19:00:38

Excessive warnings thrown for `spin -run`

#2 2020-07-31 21:49:55

Re: Excessive warnings thrown for `spin -run`

#3 2020-07-31 23:05:08

Re: Excessive warnings thrown for `spin -run`

#4 2020-08-01 04:14:01

Re: Excessive warnings thrown for `spin -run`

Board footer