diff mbox

[Ada] Remove spurious warning in Alfa mode

Message ID 20111202145027.GA25668@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Dec. 2, 2011, 2:50 p.m. UTC
The side effect removal machinery may generate illegal Ada code to avoid the
usage of access types and 'reference in Alfa mode. Since this is legal code
with respect to theorem proving, do not emit the warning.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-12-02  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Check_Initialization): Do not emit warning on
	initialization of limited type object in Alfa mode.
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 181914)
+++ sem_ch3.adb	(working copy)
@@ -9704,10 +9704,26 @@ 
                  ("?cannot initialize entities of limited type!", Exp);
 
             elsif Ada_Version < Ada_2005 then
-               Error_Msg_N
-                 ("cannot initialize entities of limited type", Exp);
-               Explain_Limited_Type (T, Exp);
 
+               --  The side effect removal machinery may generate illegal Ada
+               --  code to avoid the usage of access types and 'reference in
+               --  Alfa mode. Since this is legal code with respect to theorem
+               --  proving, do not emit the error.
+
+               if Alfa_Mode
+                 and then Nkind (Exp) = N_Function_Call
+                 and then Nkind (Parent (Exp)) = N_Object_Declaration
+                 and then not Comes_From_Source
+                                (Defining_Identifier (Parent (Exp)))
+               then
+                  null;
+
+               else
+                  Error_Msg_N
+                    ("cannot initialize entities of limited type", Exp);
+                  Explain_Limited_Type (T, Exp);
+               end if;
+
             else
                --  Specialize error message according to kind of illegal
                --  initial expression.