added concat of headers as a build output

[isubasinghe]

Motivation

These artefacts are needed as part of the verification pipeline, these concatenated files are cleaned and then fed into the C parser.

[Ivan-Velickovic]

I've changed the build to produce main_verification.c so it's obvious what it's for. With the seL4 kernel build artifacts it's hard to know with the naming convention what is used for what. Any opinions @lsf37 before I merge?

[lsf37]

No opinions from me on that one. Ideally, the concatenated C file that the verification sees should also be what the compiler gets, unless you are also planning to do binary verification. We're no longer doing that for the kernel (there it's because of BV), but if you want to eliminate the preprocessor from the trust chain, then that's the way to do it.

[Ivan-Velickovic]

No opinions from me on that one. Ideally, the concatenated C file that the verification sees should also be what the compiler gets

Okay yes we should definitely do that then. Thanks.

[Ivan-Velickovic]

Going to close this for now and re-open/make a new PR once the verification for Microkit is caught up to speed with the latest Microkit and we start working on adding verification checks for libmicrokit to the CI.