Development Log

  • SPARK Pro
    Dec 7th, 2016

    Only check component subtype at first declaration
    GNATprove now only checks subtype indications on record components when verifying the declaration of the first record type defining this component. This avoids having multiple checks on record component subtype indications, some of which could be undischarged due to missing information.