Development Log

  • SPARK Pro
    May 29th, 2017

    Better precision on functions returning tagged types
    GNATprove now tracks better the value of the tag of the result of function calls. This will lead to more discharged checks on code dealing with functions returning tagged types.