DF-5090 / proof.log
== A. no driver_t / DRIVER_MODULE / devclass registers the name 'rue' ==
sys/bus/u4b/net/ruephy.c:101: "rue") == 0)
sys/dev/netif/mii_layer/ruephy.c:96: if (strcmp(device_get_name(parent), "rue") != 0)
== B. no 'device rue' in any kernel config / platform ==
== C. no if_rue / rue module source exists anywhere ==
== D. the u4b copy of ruephy.c is an orphan (never compiled) ==
== E. the mii_layer copy IS compiled into miibus ==
== F. latent family patterns present in the audited file ==
if ((sc->mii_capabilities & BMSR_MEDIAMASK) == 0)
kprintf("no media present");
else
mii_phy_add_media(sc);
kprintf("\n");
KASSERT(IFM_INST(ife->ifm_media) == sc->mii_inst,
("ruephy_service: can't isolate RealTek RTL8150 PHY"));
mii->mii_media_active = mii->mii_media.ifm_cur->ifm_media;
== G. KASSERT gating: DragonFly stock configs DO enable INVARIANTS ==
#else
#define KASSERT(exp,msg) do { } while (0)
#define KKASSERT(exp) do { } while (0)
sys/config/X86_64_GENERIC: INVARIANTS count=1
sys/config/LINT64: INVARIANTS count=3
sys/config/VKERNEL64: INVARIANTS count=1
PROOF OK: probe gate (ruephy.c:96) can never pass => attach/service/status/reset
are unreachable on every kernel buildable from this tree.