Development Log

  • SPARK Pro
    Mar 30th, 2017

    Globals of renamed subprograms in code not-in-SPARK
    GNATprove now synthesizes more precise Global contracts for subprograms annotated with SPARK_Mode => Off that make calls via subprogram renamings. Such calls happen, for example, in instances of generic units with formal subprogram parameters.