Prag : Node_Id;
begin
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related package body.
+
Save_SPARK_Mode_And_Set (Body_Id, Mode);
Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
Error_Msg_N ("package & requires state refinement", Spec_Id);
end if;
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
Restore_SPARK_Mode (Mode);
end Analyze_Package_Body_Contract;
Prag : Node_Id;
begin
+ -- Due to the timing of contract analysis, delayed pragmas may be
+ -- subject to the wrong SPARK_Mode, usually that of the enclosing
+ -- context. To remedy this, restore the original SPARK_Mode of the
+ -- related package.
+
Save_SPARK_Mode_And_Set (Pack_Id, Mode);
-- Analyze the initialization related pragmas. Initializes must come
end if;
end if;
+ -- Restore the SPARK_Mode of the enclosing context after all delayed
+ -- pragmas have been analyzed.
+
Restore_SPARK_Mode (Mode);
end Analyze_Package_Contract;