Development Log

  • SPARK Pro
    Dec 21st, 2016

    More precise analysis for exclusive use of entries
    Tasks were previously only allowed to call the same entry if they were using entries belonging to different (library-level) objects. Now GNATprove also accepts calls from more than one task to a single entry provided that each task uses an entry belonging to a different component of a record object.