Open
Description
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.html
So 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!