> On 4 May 2021, at 13:11, Matthew Fernandez <[email protected]>
> wrote:
>
>
>> On May 3, 2021, at 04:57, Ben Fiedler <[email protected]> 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.
>
> [0]: https://github.com/seL4/pruner
Just to confirm: this is still the way to go, AFAIK.
Cheers,
Gerwin
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
