Miscellaneous warnings in generated C code
franziskuskiefer opened this issue · 2 comments
Tracking issue to fix miscellaneous warnings in generated C code.
See hacl-star/hacl-star#843 for a list of warnings.
The following patch proposed by @protz works well for all the unused-but-set warnings in HACL*.
diff --git a/dist/karamel/include/krml/internal/target.h b/dist/karamel/include/krml/internal/target.h
index 9eb260c630..a378ed4f4b 100644
--- a/dist/karamel/include/krml/internal/target.h
+++ b/dist/karamel/include/krml/internal/target.h
@@ -169,6 +169,7 @@ inline static int32_t krml_time(void) {
#define KRML_LOOP1(i, n, x) { \
x \
i += n; \
+ (void) i; \
}
#define KRML_LOOP2(i, n, x) \
With the latest round of fixes regarding possibly unused variables, the code now compiles with the following flags:
Lines 15 to 17 in da83fc3
namely, -Wall -Wextra -Werror with the addition of -Wno-infinite-recursion since F* doesn't prevent this by default.
Now there are MANY more warnings beyond those enabled by -Wall and -Wextra -- see https://gcc.gnu.org/onlinedocs/gcc/Warning-Options.html for instance. Those should be discussed on a case-by-base basis, because there's no consensus that these "extra extra" warnings are helpful. I'm thinking for instance about -Wpedantic, which gives this:
./curve25519-inline.h:218:5: error: string literal of length 4266 exceeds maximum length 4095 that ISO C99 compilers are required to support [-Werror,-Woverlength-strings]
" movq 0(%0), %%rdx;"
^~~~~~~~~~~~~~~~~~~~~~
in the build of HACL, or -Wimplicit-int-conversions which gives a TON of errors, most of which are innocuous (in particular, since #387, assignments of uint8 or uint16 computations always triggers a warning).
Conversely, some warnings are enabled by -Wextra -Wall but it's up to the user to do something about it, since krml won't work around them (thinking about -Wset-but-unused for instancen which krml could conceivably work to defeat, but again, better to discuss in a specific issue).
So I'm closing this, but happy to discuss any new issue about a specific C compiler warning that krml should guard against (i.e., make sure is never triggered).