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
While trying to minimize the generated C code for @NikolajBjorner:
too many files include libintvector.h indiscriminately
evercrypt_targetconfig.h, ibid.
kremlib (minimal) depends on compat.h which is nonsensical -- all of the stuff that mentions Prims from the machine integers should just be marked as noextract
cruft shipped in the kremlib directories: Makefile.{basic,include} and .def file
lots of stuff in types.h that should go in "full" kremlib, or maybe not even be there except for bootstrapping?
purpose of KRML_HOST_SNPRINTF?
excessive inclusion of Hacl_Kremlib.h in numerous files... spurious?
too many unused variable errors -- maintaining a list in Helpers.ml that's hardcoded is not scalable, can we add an F* attribute somewhere for assumed definitions that in addition to assuming their types, assume that they are pure for the sake of triggering kremlin's unused variable elimination?
The text was updated successfully, but these errors were encountered:
While trying to minimize the generated C code for @NikolajBjorner:
Hacl_Kremlib.h
in numerous files... spurious?The text was updated successfully, but these errors were encountered: