Behavioral regressions behind an unchanged declaration¶
Index: Known gaps
Status (re-verified 2026-10-09 at 456989f): POLICY_NOTE. case208 ground truth records behavioral_break with truth_scope declared-interface and no detector expected. An L4 definition/declaration restrict replay is an unimplemented enhancement, not a regression.
Catalog case208 (restrict added to a function definition only) breaks a
valid overlapping consumer at runtime under GCC and Clang, while the
declared interface — everything a binary/header comparison reads — is
identical. Ground truth records it as behavioral_break: true with
truth_scope: declared-interface; no detector is expected to infer it.
An L4 source-ABI replay could see restrict on the definition's
parameters and report a definition/declaration contract mismatch; that is
not implemented.