Merge pull request #1238 from pq-code-package/conv-warnings-again

hanno-becker · web-flow · commit 6048cab06ffb · 2025-10-19T19:11:04.000+01:00
Add explicit signed -&gt; unsigned conversion
diff --git a/examples/basic/Makefile b/examples/basic/Makefile
@@ -60,6 +60,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/basic_deterministic/Makefile b/examples/basic_deterministic/Makefile
@@ -48,6 +48,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/bring_your_own_fips202/Makefile b/examples/bring_your_own_fips202/Makefile
@@ -66,6 +66,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/custom_backend/Makefile b/examples/custom_backend/Makefile
@@ -63,6 +63,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/monolithic_build/Makefile b/examples/monolithic_build/Makefile
@@ -68,6 +68,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/monolithic_build_multilevel_native/Makefile b/examples/monolithic_build_multilevel_native/Makefile
@@ -96,6 +96,7 @@ CFLAGS := \
 	-Wno-unknown-pragmas \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-unused-command-line-argument \
 	-fomit-frame-pointer \
 	-std=c99 \
diff --git a/examples/monolithic_build_native/Makefile b/examples/monolithic_build_native/Makefile
@@ -104,6 +104,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/multilevel_build/Makefile b/examples/multilevel_build/Makefile
@@ -86,6 +86,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/examples/multilevel_build_native/Makefile b/examples/multilevel_build_native/Makefile
@@ -62,6 +62,7 @@ CFLAGS := \
 	-Wpointer-arith \
 	-Wredundant-decls \
 	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \
diff --git a/mlkem/src/poly.h b/mlkem/src/poly.h
@@ -102,8 +102,9 @@ __contract__(
   /* check-magic: 62209 == unsigned_mod(pow(MLKEM_Q, -1, 2^16), 2^16) */
   const uint32_t QINV = 62209;
 
-  /*  Compute a*q^{-1} mod 2^16 in unsigned representatives */
-  const uint16_t a_reduced = (uint16_t)(a & UINT16_MAX);
+  /* Compute a*q^{-1} mod 2^16 in unsigned representatives. */
+  const uint16_t a_reduced = (uint16_t)(a & (int32_t)UINT16_MAX);
+
   const uint16_t a_inverted = (a_reduced * QINV) & UINT16_MAX;
 
   /* Lift to signed canonical representative mod 2^16. */
diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h
@@ -191,16 +191,6 @@ __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF)))
 #pragma CPROVER check pop
 #endif
 
-/*
- * The mlk_ct_cmask_neg_i16 function below makes deliberate use of
- * signed to unsigned integer conversion, which is fully defined
- * behaviour in C. It is thus safe to disable this warning.
- */
-#ifdef CBMC
-#pragma CPROVER check push
-#pragma CPROVER check disable "conversion"
-#endif
-
 /*************************************************
  * Name:        mlk_ct_cmask_neg_i16
  *
@@ -227,14 +217,9 @@ __contract__(ensures(return_value == ((x < 0) ? 0xFFFF : 0)))
   /* This truncation does alter the value of tmp. We deliberately
    * rely on the defined behavior of signed-to-unsigned conversion
    * for negative inputs. */
-  return (uint16_t)tmp;
+  return (uint16_t)(tmp & (int32_t)UINT16_MAX);
 }
 
-/* Put unsigned-to-signed warnings in CBMC back into scope */
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
 /*
  * The ct_csel_xxx functions below make deliberate use of unsigned
  * to signed integer conversion, which is implementation-defined
