-
Notifications
You must be signed in to change notification settings - Fork 228
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Any options available for function & data purging? #500
Comments
There's a way to eliminate unreferenced functions at link-time, but it's not very convenient. In the C source, you can annotate function definitions with the
Then you can link with It would definitely be more convenient to have compile-time flags |
Thanks for your reply! I do agree manually annotating each function with the attribute here works. However it is still editing the code, another path I can employ, is simply eliminating those code that is not called :P In our case, it is not so hard to locate all the functions that can be removed. That being said, I was still hoping we could automate this process somehow, since we are still talking about changing a non-trivial third party library being used, it might not be the best idea to always have to maintain a fork where we either 1) add annotations to each function; or 2) delete a significant portion of all code. Perhaps it might be possible to build something like a preprocessor that automatically annotate each function? Not sure but I will look into this path. And I totally understand that it might or might not be a non-trivial task to introduce those flags in CompCert. |
After some time digging into the internals of CompCert(well, my original plan is to write a pre-processor using libclang that adds those attributes automatically, but in the end decided that hacking CompCert is actually easier :P), I've managed to put together a patch that introduces
Still, I do want to check here: is this a path that makes sense to proceed? Or do you have other concerns in mind? |
Hi,
I noticed that CompCert does not yet support
-ffunction-sections
and-fdata-sections
, which are typically used to purge unused functions / data in gcc / clang: https://gcc.gnu.org/onlinedocs/gnat_ugn/Compilation-options.htmlSo one question I have here, is there any option in CompCert where we can achieve similar behavior? I know one alternative is that we can manually eliminate functions that will not be called but for bigger libraries, this might be a large amount of work. So I was curious if there is a way we can achieve this via tweaking compiler flags.
Many thanks!
The text was updated successfully, but these errors were encountered: