Development Log

  • SPARK Pro
    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.