Jun 28th, 2017
No inlining of subprograms visible to child packages
GNATprove no longer inlines subprograms declared in private parts of package specifications as part of its "Contextual Analysis of Subprograms without Contracts" feature (which is documented in the SPARK User's Gude). Such inlining could be confusing for the users, because the same code could be provable if located in a package body, but not provable if located in a child package. As a result a spurious warning of the form "analyzing unreferenced procedure" for subprograms visible to child packages is no longer emitted.