[seL4] Re: Generating CAmkES glue-spec and glue-proofs

On May 3, 2021, at 04:57, Ben Fiedler wrote:

I'm trying to feed the CAmkES-generated code to AutoCorres, but it's (seemingly) unhappy somewhere in the underlying musllibc code. I suspect that Isabelle's C parser doesn't understand variadic function arguments and trips over the va_list definition. Have you experienced this as well, and if so how did you solve it? I peeked at another (non-seL4) project of ours and it dealt with these issues by ifdef'ing the relevant imports, so that all relevant code is self-contained.

In the past, this was something I dealt with using a hack known as the pruner [0]. These days there may be a better option. [0]: https://github.com/seL4/pruner