search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

added concat of headers as a build output #84

Open isubasinghe opened 7 months ago

isubasinghe commented 7 months ago

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 commented 7 months ago

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 commented 7 months ago

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 commented 7 months ago

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.