This patch clarifies the need of saving and restoring SPARK_Mode in a stack
like fashion. No change in behavior, no test needed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-17 Hristian Kirtchev
* sem_ch6.adb (Analyze_Subprogram_Body_Contract,
Analyze_Subprogram_C
This patch ensures that all delayed SPARK aspects are analyzed with the proper
SPARK mode of their related construct.
-- Source --
-- modes.ads
package Modes
with SPARK_Mode => On,
Abstract_State => State
is
Var : Integer := 1;
procedure Disabled_1 (For
