Resolve -Wconversion and -Wsign-conversion warnings #552
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mkannwischer
force-pushed
the
wconversion
branch
4 times, most recently
from
878529f to
776981c
Compare
hanno-becker
requested changes
Oct 24, 2025
There was a problem hiding this comment.
Thank you @mkannwischer for embarking on this! There are a few cases where I think we should document why the cast is safe, or try to avoid it altogether. Otherwise, we may as well leave the warnings off.
mkannwischer
force-pushed
the
wconversion
branch
2 times, most recently
from
51a6d72 to
3b6dd16
Compare
mkannwischer
force-pushed
the
wconversion
branch
2 times, most recently
from
85beb05 to
3858af1
Compare
hanno-becker
force-pushed
the
wconversion
branch
from
3858af1 to
5ed3488
Compare
hanno-becker
approved these changes
Oct 25, 2025
There was a problem hiding this comment.
Thank you @mkannwischer, this is definitely an improvement. I quite like how the conversion warnings force you to think about the bounds.
This commit introduces helper functions mld_cast_uint32_to_int32, mld_cast_int32_to_uint32, and mld_cast_int64_to_uint32 for int64_t->uint32_t, and int32_t <-> uint32_t. This cleans up prior code and also removes the need for some pragmas stopping CBMC from flagging value-changing integer conversions. This commit is based on pq-code-package/mlkem-native@e5adf3a (but for 32-bit integers. Signed-off-by: Matthias J. Kannwischer <[email protected]>
This commit enables additional warnings (-Wconversion, -Wsign-conversions) requiring more explicit casts. All of those casts should already be safe as checked by CBMC. Resolves #543 Signed-off-by: Matthias J. Kannwischer <[email protected]>
Since the addition of -Wconversion and -Wsign-conversion to the default CFLAGS, compilation of the CMSIS files for AN547 fails. This commit allows custom Makefiles to not only provide EXTRA_SOURCES to specify additional sources, but also EXTRA_SOURCES_CFLAGS for additional CFLAGS, which in particular may overwrite default CFLAGS (they apply later). This is leveraged in the case of m55-an547/platform.mk to disable conversion and sign-conversion warnings for all CMSIS files. Port of pq-code-package/mlkem-native@15fa58e Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
force-pushed
the
wconversion
branch
from
5ed3488 to
786e8f6
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit enables additional warnings (-Wconversion, -Wsign-conversions) requiring more explicit casts.
All of those casts should already be safe as checked by CBMC.
-Wconversionand-Wsign-conversionwarnings (and resolve findings) #543