On 4 May 2021, at 13:11, Matthew Fernandez
wrote: 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.
That's correct, yes, varargs are not in the verification subset for C.
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.
Just to confirm: this is still the way to go, AFAIK. Cheers, Gerwin