Development Log

  • SPARK Pro
    May 31st, 2017

    Improve message for overridden subprograms
    When an overriding subprogram has more effects on globals variables than the overridden subprogram, GNATprove will report an error message. We have now improved this message making more explicit the underlying issue and we have reworded the case when these effects are through access types (i.e. pointers).