Development Log

  • SPARK Pro
    May 10th, 2017

    Precise handling of dispatching calls with known tag
    GNATprove now precisely determines the subprogram called by a dispatching call when the tag is known. In particular, it is now able to use its more precise specific contract if any.