You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I have been compiling MPS on Linux using GCC 11.4 for a while. Around version 11 (I'm unsure exactly when), the following warning started appearing:
In file included from /home/filip/Projects/storm/mps/code/mps.c:34,
from /home/filip/Projects/storm/Gc/MPS/Lib.c:21:
/home/filip/Projects/storm/mps/code/mpm.c: In function ‘WriteULongest.constprop’:
/home/filip/Projects/storm/mps/code/mpm.c:295:12: warning: ‘__builtin_memset’ forming offset [65, 4294967294] is out of the bounds [0, 65] of object ‘buf’ with type ‘char[65]’ [-Warray-bounds]
295 | buf[i] = pad;
| ~~~~~~~^~~~~
/home/filip/Projects/storm/mps/code/mpm.c:269:8: note: ‘buf’ declared here
269 | char buf[MPS_WORD_WIDTH + 1]; /* enough for binary, */
| ^~~
It looks like it has found a possible bug in the number formatting code, but my manual inspection tells me it is correct. The warning appears under -O3 -Wall -Wextra, but not under -O2. Furthermore, using clang with -O3 -Wall -Wextra does not cause any warnings. This makes me suspect a bug in GCC, but I am not sure. I will report it to GCC as well and see what happens.
Isolating the code into a separate file, I have further narrowed the problem down. The warning only appears when width is zero or one, and when constants are propagated into the function (as indicated by the name in the warning). The warning also disappears if the loop that pads the output is surrounded by an if (width > 1).
I vaguely remember that you do not officially support -O3, so this might not be relevant. Since it could point to an issue that I fail to see, I thought I'd bring it to your attention at least. I have fixed the issue by adding the above-mentioned check. Since it is not on a critical path, it should not be an issue performance-wise, even if it makes the code a bit less elegant. The link is below if it is of interest to you: fstromback@61e4908
The text was updated successfully, but these errors were encountered:
I have been compiling MPS on Linux using GCC 11.4 for a while. Around version 11 (I'm unsure exactly when), the following warning started appearing:
It looks like it has found a possible bug in the number formatting code, but my manual inspection tells me it is correct. The warning appears under
-O3 -Wall -Wextra
, but not under-O2
. Furthermore, using clang with-O3 -Wall -Wextra
does not cause any warnings. This makes me suspect a bug in GCC, but I am not sure. I will report it to GCC as well and see what happens.Isolating the code into a separate file, I have further narrowed the problem down. The warning only appears when
width
is zero or one, and when constants are propagated into the function (as indicated by the name in the warning). The warning also disappears if the loop that pads the output is surrounded by anif (width > 1)
.I vaguely remember that you do not officially support
-O3
, so this might not be relevant. Since it could point to an issue that I fail to see, I thought I'd bring it to your attention at least. I have fixed the issue by adding the above-mentioned check. Since it is not on a critical path, it should not be an issue performance-wise, even if it makes the code a bit less elegant. The link is below if it is of interest to you: fstromback@61e4908The text was updated successfully, but these errors were encountered: