Hi Julien,
Yes, I would go with 3., replace advance_pc with domain_crash.
Assuming
that it would also solve the violation in ECLAIR.
It needs to be prefixed with an ASSERT_UNREACHABLE(), though, because
it's still a violation if there is no execution path leading to
domain_crash(), but other than that it seems the safest choice.
Assuming there are no objections to going forward with this proposal,
would you mind telling me how can I do the proper domain_crash call.
Most of the examples get a "struct domain *" from a parameter or from
the macro "current", so I was thinking of
domain_crash(current->domain);
but I'm not so sure about this, as there are no other uses in vcpreg.c.
You can also submit the patch yourself, if you prefer.
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)