Commit efd3c368 by Arnaud Charlet

Update comments

From-SVN: r212819
parent 4b03d946
...@@ -184,6 +184,11 @@ package body Sem_Ch7 is ...@@ -184,6 +184,11 @@ package body Sem_Ch7 is
Prag : Node_Id; Prag : Node_Id;
begin 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); Save_SPARK_Mode_And_Set (Body_Id, Mode);
Prag := Get_Pragma (Body_Id, Pragma_Refined_State); Prag := Get_Pragma (Body_Id, Pragma_Refined_State);
...@@ -204,6 +209,9 @@ package body Sem_Ch7 is ...@@ -204,6 +209,9 @@ package body Sem_Ch7 is
Error_Msg_N ("package & requires state refinement", Spec_Id); Error_Msg_N ("package & requires state refinement", Spec_Id);
end if; end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Restore_SPARK_Mode (Mode); Restore_SPARK_Mode (Mode);
end Analyze_Package_Body_Contract; end Analyze_Package_Body_Contract;
...@@ -848,6 +856,11 @@ package body Sem_Ch7 is ...@@ -848,6 +856,11 @@ package body Sem_Ch7 is
Prag : Node_Id; Prag : Node_Id;
begin 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); Save_SPARK_Mode_And_Set (Pack_Id, Mode);
-- Analyze the initialization related pragmas. Initializes must come -- Analyze the initialization related pragmas. Initializes must come
...@@ -876,6 +889,9 @@ package body Sem_Ch7 is ...@@ -876,6 +889,9 @@ package body Sem_Ch7 is
end if; end if;
end if; end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
Restore_SPARK_Mode (Mode); Restore_SPARK_Mode (Mode);
end Analyze_Package_Contract; end Analyze_Package_Contract;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment