Development Log

  • SPARK Pro
    Apr 17th, 2016

    More flexible elaboration rules with static model
    GNATprove now implements a more flexible enforcement of SPARK elaboration rules, that does not always requires Elaborate_All for calls and reads of subprograms and variables defined in other units during elaboration. Specifically, when the static elaboration model of GNAT is used (i.e. when neither switch -gnatE nor pragma Elaboration_Checks (Dynamic) are used), the more powerful mechanism of the compiler is used to compute a safe elaboration order for calls across units during elaboration, and GNATprove only requires the use of Elaborate_Body on units that modify the value of library-level variables defined in the spec during the elaboration of the unit body (SPARK RM rule 7.7.1(5)).