From e1e307d94145e51d9a06448466fbb1a535c89a38 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 16 Oct 2015 15:43:47 +0200 Subject: [PATCH] [multiple changes] 2015-10-16 Hristian Kirtchev * sem_ch12.adb (Analyze_Package_Instantiation): Treat a missing SPARK_Mode annotation as having mode "Off". (Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode annotation as having mode "Off". (Instantiate_Package_Body): Code reformatting. Treat a missing SPARK_Mode annotation as having mode "Off". (Instantiate_Subprogram_Body): Code reformatting. Treat a missing SPARK_Mode annotation as having mode "Off". 2015-10-16 Ed Schonberg * exp_ch5.adb: Code clean up. * sem_ch13.adb: Minor fix in comment. 2015-10-16 Bob Duff * a-exexda.adb: Change format of Exception_Information to be more like what we print for unhandled exceptions. * a-exstat.adb: Parse new format. * a-except-2005.adb, a-except.adb: Document new format. From-SVN: r228907 --- gcc/ada/ChangeLog | 24 ++++++ gcc/ada/a-except-2005.adb | 4 +- gcc/ada/a-except.adb | 4 +- gcc/ada/a-exexda.adb | 14 ++-- gcc/ada/a-exstat.adb | 170 ++++++++++++++++++++------------------ gcc/ada/exp_ch5.adb | 5 +- gcc/ada/sem_ch12.adb | 62 ++++++++++---- gcc/ada/sem_ch13.adb | 2 +- 8 files changed, 173 insertions(+), 112 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d8f2b58a107..751cbf7df2e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,27 @@ +2015-10-16 Hristian Kirtchev + + * sem_ch12.adb (Analyze_Package_Instantiation): + Treat a missing SPARK_Mode annotation as having mode "Off". + (Analyze_Subprogram_Instantiation): Treat a missing SPARK_Mode + annotation as having mode "Off". + (Instantiate_Package_Body): Code + reformatting. Treat a missing SPARK_Mode annotation as having mode + "Off". + (Instantiate_Subprogram_Body): Code reformatting. Treat + a missing SPARK_Mode annotation as having mode "Off". + +2015-10-16 Ed Schonberg + + * exp_ch5.adb: Code clean up. + * sem_ch13.adb: Minor fix in comment. + +2015-10-16 Bob Duff + + * a-exexda.adb: Change format of Exception_Information to be + more like what we print for unhandled exceptions. + * a-exstat.adb: Parse new format. + * a-except-2005.adb, a-except.adb: Document new format. + 2015-10-16 Javier Miranda * sem_ch5.adb (Analyze_Iterator_Specification): Associate a diff --git a/gcc/ada/a-except-2005.adb b/gcc/ada/a-except-2005.adb index 10f06bfd931..e7929178061 100644 --- a/gcc/ada/a-except-2005.adb +++ b/gcc/ada/a-except-2005.adb @@ -152,8 +152,8 @@ package body Ada.Exceptions is -- -- The format of the string is as follows: -- - -- Exception_Name: (as in Exception_Name) - -- Message: (only if Exception_Message is empty) + -- raised : + -- (" : " is present only if Exception_Message is not empty) -- PID=nnnn (only if nonzero) -- Call stack traceback locations: (only if at least one location) -- <0xyyyyyyyy 0xyyyyyyyy ...> (is recorded) diff --git a/gcc/ada/a-except.adb b/gcc/ada/a-except.adb index 67609828cba..a228a8395fe 100644 --- a/gcc/ada/a-except.adb +++ b/gcc/ada/a-except.adb @@ -117,8 +117,8 @@ package body Ada.Exceptions is -- -- The format of the string is as follows: -- - -- Exception_Name: (as in Exception_Name) - -- Message: (only if Exception_Message is empty) + -- raised : + -- (" : " is present only if Exception_Message is not empty) -- PID=nnnn (only if nonzero) -- Call stack traceback locations: (only if at least one location) -- <0xyyyyyyyy 0xyyyyyyyy ...> (is recorded) diff --git a/gcc/ada/a-exexda.adb b/gcc/ada/a-exexda.adb index c3d17189568..2a5ffbcf20e 100644 --- a/gcc/ada/a-exexda.adb +++ b/gcc/ada/a-exexda.adb @@ -248,11 +248,11 @@ package body Exception_Data is -- Append_Info_Basic_Exception_Information -- --------------------------------------------- - -- To ease the maximum length computation, we define and pull out a couple - -- of string constants: + -- To ease the maximum length computation, we define and pull out some + -- string constants: - BEI_Name_Header : constant String := "Exception name: "; - BEI_Msg_Header : constant String := "Message: "; + BEI_Name_Header : constant String := "raised "; + BEI_Msg_Header : constant String := " : "; BEI_PID_Header : constant String := "PID: "; procedure Append_Info_Basic_Exception_Information @@ -275,13 +275,13 @@ package body Exception_Data is if Name (Name'First) /= '_' then Append_Info_String (BEI_Name_Header, Info, Ptr); Append_Info_String (Name, Info, Ptr); - Append_Info_NL (Info, Ptr); if Exception_Message_Length (X) /= 0 then Append_Info_String (BEI_Msg_Header, Info, Ptr); Append_Info_Exception_Message (X, Info, Ptr); - Append_Info_NL (Info, Ptr); end if; + + Append_Info_NL (Info, Ptr); end if; -- Output PID line if nonzero @@ -498,7 +498,7 @@ package body Exception_Data is is begin return - BEI_Name_Header'Length + Exception_Name_Length (X) + 1 + BEI_Name_Header'Length + Exception_Name_Length (X) + BEI_Msg_Header'Length + Exception_Message_Length (X) + 1 + BEI_PID_Header'Length + 15; end Basic_Exception_Info_Maxlength; diff --git a/gcc/ada/a-exstat.adb b/gcc/ada/a-exstat.adb index b1c6db3a557..1ff9481eb14 100644 --- a/gcc/ada/a-exstat.adb +++ b/gcc/ada/a-exstat.adb @@ -142,117 +142,125 @@ package body Stream_Attributes is begin if S = "" then return Null_Occurrence; + end if; - else - To := S'First - 2; - Next_String; + To := S'First - 2; + Next_String; - if S (From .. From + 15) /= "Exception name: " then - Bad_EO; - end if; - - X.Id := Exception_Id (Internal_Exception (S (From + 16 .. To))); + if S (From .. From + 6) /= "raised " then + Bad_EO; + end if; - Next_String; + declare + Name_Start : constant Positive := From + 7; + begin + From := Name_Start + 1; - if From <= To and then S (From) = 'M' then - if S (From .. From + 8) /= "Message: " then - Bad_EO; - end if; + while From < To and then S (From) /= ' ' loop + From := From + 1; + end loop; - X.Msg_Length := To - From - 8; - X.Msg (1 .. X.Msg_Length) := S (From + 9 .. To); - Next_String; + X.Id := + Exception_Id (Internal_Exception (S (Name_Start .. From - 1))); + end; - else - X.Msg_Length := 0; + if From <= To then + if S (From .. From + 2) /= " : " then + Bad_EO; end if; - X.Pid := 0; - - if From <= To and then S (From) = 'P' then - if S (From .. From + 3) /= "PID:" then - Bad_EO; - end if; + X.Msg_Length := To - From - 2; + X.Msg (1 .. X.Msg_Length) := S (From + 3 .. To); - From := From + 5; -- skip past PID: space + else + X.Msg_Length := 0; + end if; - while From <= To loop - X.Pid := X.Pid * 10 + - (Character'Pos (S (From)) - Character'Pos ('0')); - From := From + 1; - end loop; + Next_String; + X.Pid := 0; - Next_String; + if From <= To and then S (From) = 'P' then + if S (From .. From + 3) /= "PID:" then + Bad_EO; end if; - X.Num_Tracebacks := 0; - - if From <= To then - if S (From .. To) /= "Call stack traceback locations:" then - Bad_EO; - end if; + From := From + 5; -- skip past PID: space - Next_String; - loop - exit when From > To; + while From <= To loop + X.Pid := X.Pid * 10 + + (Character'Pos (S (From)) - Character'Pos ('0')); + From := From + 1; + end loop; - declare - Ch : Character; - C : Integer_Address; - N : Integer_Address; - - begin - if S (From) /= '0' - or else S (From + 1) /= 'x' - then - Bad_EO; - else - From := From + 2; - end if; + Next_String; + end if; - C := 0; - while From <= To loop - Ch := S (From); + X.Num_Tracebacks := 0; - if Ch in '0' .. '9' then - N := - Character'Pos (S (From)) - Character'Pos ('0'); + if From <= To then + if S (From .. To) /= "Call stack traceback locations:" then + Bad_EO; + end if; - elsif Ch in 'a' .. 'f' then - N := - Character'Pos (S (From)) - Character'Pos ('a') + 10; + Next_String; + loop + exit when From > To; + + declare + Ch : Character; + C : Integer_Address; + N : Integer_Address; + + begin + if S (From) /= '0' + or else S (From + 1) /= 'x' + then + Bad_EO; + else + From := From + 2; + end if; - elsif Ch = ' ' then - From := From + 1; - exit; + C := 0; + while From <= To loop + Ch := S (From); - else - Bad_EO; - end if; + if Ch in '0' .. '9' then + N := + Character'Pos (S (From)) - Character'Pos ('0'); - C := C * 16 + N; + elsif Ch in 'a' .. 'f' then + N := + Character'Pos (S (From)) - Character'Pos ('a') + 10; + elsif Ch = ' ' then From := From + 1; - end loop; + exit; - if X.Num_Tracebacks = Max_Tracebacks then + else Bad_EO; end if; - X.Num_Tracebacks := X.Num_Tracebacks + 1; - X.Tracebacks (X.Num_Tracebacks) := - TBE.TB_Entry_For (To_Address (C)); - end; - end loop; - end if; + C := C * 16 + N; - -- If an exception was converted to a string, it must have - -- already been raised, so flag it accordingly and we are done. + From := From + 1; + end loop; - X.Exception_Raised := True; - return X; + if X.Num_Tracebacks = Max_Tracebacks then + Bad_EO; + end if; + + X.Num_Tracebacks := X.Num_Tracebacks + 1; + X.Tracebacks (X.Num_Tracebacks) := + TBE.TB_Entry_For (To_Address (C)); + end; + end loop; end if; + + -- If an exception was converted to a string, it must have + -- already been raised, so flag it accordingly and we are done. + + X.Exception_Raised := True; + return X; end String_To_EO; end Stream_Attributes; diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb index 29113e5c863..8a90b6c1fb7 100644 --- a/gcc/ada/exp_ch5.adb +++ b/gcc/ada/exp_ch5.adb @@ -2956,6 +2956,10 @@ package body Exp_Ch5 is Prepend (Elmt_Ref, Stats); + -- The element is assignable in the expanded code. + + Set_Assignment_OK (Name (Elmt_Ref)); + -- The loop is rewritten as a block, to hold the element declaration New_Loop := @@ -2981,7 +2985,6 @@ package body Exp_Ch5 is Analyze (Elmt_Decl); Set_Ekind (Defining_Identifier (Elmt_Decl), E_Loop_Parameter); - Set_Assignment_OK (Name (Elmt_Ref)); Analyze (N); end Expand_Formal_Container_Element_Loop; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 94b2a392771..6bcecf4b8da 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3723,11 +3723,12 @@ package body Sem_Ch12 is goto Leave; else - -- If the context of the instance is subject to SPARK_Mode "off", - -- set the global flag which signals Analyze_Pragma to ignore all - -- SPARK_Mode pragmas within the instance. + -- If the context of the instance is subject to SPARK_Mode "off" or + -- the annotation is altogether missing, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within + -- the instance. - if SPARK_Mode = Off then + if SPARK_Mode /= On then Ignore_Pragma_SPARK_Mode := True; end if; @@ -5098,11 +5099,12 @@ package body Sem_Ch12 is Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit); else - -- If the context of the instance is subject to SPARK_Mode "off", - -- set the global flag which signals Analyze_Pragma to ignore all - -- SPARK_Mode pragmas within the instance. + -- If the context of the instance is subject to SPARK_Mode "off" or + -- the annotation is altogether missing, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within + -- the instance. - if SPARK_Mode = Off then + if SPARK_Mode /= On then Ignore_Pragma_SPARK_Mode := True; end if; @@ -10632,17 +10634,18 @@ package body Sem_Ch12 is Act_Spec : constant Node_Id := Specification (Act_Decl); Act_Decl_Id : constant Entity_Id := Defining_Entity (Act_Spec); + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + Save_Style_Check : constant Boolean := Style_Check; + + Act_Body : Node_Id; + Act_Body_Id : Entity_Id; Act_Body_Name : Node_Id; Gen_Body : Node_Id; Gen_Body_Id : Node_Id; - Act_Body : Node_Id; - Act_Body_Id : Entity_Id; + Par_Ent : Entity_Id := Empty; + Par_Vis : Boolean := False; Parent_Installed : Boolean := False; - Save_Style_Check : constant Boolean := Style_Check; - - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation @@ -10783,8 +10786,17 @@ package body Sem_Ch12 is if Present (Gen_Body_Id) then Save_Env (Gen_Unit, Act_Decl_Id); Style_Check := False; - Current_Sem_Unit := Body_Info.Current_Sem_Unit; + -- If the context of the instance is subject to SPARK_Mode "off" or + -- the annotation is altogether missing, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within + -- the instance. + + if SPARK_Mode /= On then + Ignore_Pragma_SPARK_Mode := True; + end if; + + Current_Sem_Unit := Body_Info.Current_Sem_Unit; Gen_Body := Unit_Declaration_Node (Gen_Body_Id); Create_Instantiation_Source @@ -10943,6 +10955,7 @@ package body Sem_Ch12 is end if; Restore_Env; + Ignore_Pragma_SPARK_Mode := Save_IPSM; Style_Check := Save_Style_Check; -- If we have no body, and the unit requires a body, then complain. This @@ -11019,6 +11032,7 @@ package body Sem_Ch12 is Pack_Id : constant Entity_Id := Defining_Unit_Name (Parent (Act_Decl)); + Saved_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; Saved_Style_Check : constant Boolean := Style_Check; Saved_Warnings : constant Warning_Record := Save_Warnings; @@ -11104,6 +11118,16 @@ package body Sem_Ch12 is Save_Env (Gen_Unit, Anon_Id); Style_Check := False; + + -- If the context of the instance is subject to SPARK_Mode "off" or + -- the annotation is altogether missing, set the global flag which + -- signals Analyze_Pragma to ignore all SPARK_Mode pragmas within + -- the instance. + + if SPARK_Mode /= On then + Ignore_Pragma_SPARK_Mode := True; + end if; + Current_Sem_Unit := Body_Info.Current_Sem_Unit; Create_Instantiation_Source (Inst_Node, @@ -11203,6 +11227,7 @@ package body Sem_Ch12 is end if; Restore_Env; + Ignore_Pragma_SPARK_Mode := Saved_IPSM; Style_Check := Saved_Style_Check; Restore_Warnings (Saved_Warnings); @@ -11268,9 +11293,10 @@ package body Sem_Ch12 is (Make_Simple_Return_Statement (Loc, Ret_Expr)))); end if; - Pack_Body := Make_Package_Body (Loc, - Defining_Unit_Name => New_Copy (Pack_Id), - Declarations => New_List (Act_Body)); + Pack_Body := + Make_Package_Body (Loc, + Defining_Unit_Name => New_Copy (Pack_Id), + Declarations => New_List (Act_Body)); Insert_After (Inst_Node, Pack_Body); Set_Corresponding_Spec (Pack_Body, Pack_Id); diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index b820f4ddcc7..40d4d357528 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -122,7 +122,7 @@ package body Sem_Ch13 is -- to generate appropriate semantic checks that are delayed until this -- point (they had to be delayed this long for cases of delayed aspects, -- e.g. analysis of statically predicated subtypes in choices, for which - -- we have to be sure the subtypes in question are frozen before checking. + -- we have to be sure the subtypes in question are frozen before checking). function Get_Alignment_Value (Expr : Node_Id) return Uint; -- Given the expression for an alignment value, returns the corresponding -- 2.30.2