Spinroot

A forum for Spin users

You are not logged in.

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

Maxvonhippel
Member
Registered: 2019-09-13
Posts: 20

Excessive warnings thrown for `spin -run`

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!

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Excessive warnings thrown for `spin -run`

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.

Offline

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

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Excessive warnings thrown for `spin -run`

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

Offline

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

Maxvonhippel
Member
Registered: 2019-09-13
Posts: 20

Re: Excessive warnings thrown for `spin -run`

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

Offline

Board footer

Powered by FluxBB