struct vcpu { struct tcb* tcb; ...
struct arch_tcb { struct vcpu* vcpu; ...
and
struct tcb { struct arch_tcb tcbArch; ...
These conspire to generate a type error on verification side due to
assumptions about non-colliding names.
|
||
|---|---|---|
| .. | ||
| arm | ||
| x86/arch | ||