[multiple changes]

2015-10-16  Hristian Kirtchev  <kirtchev@adacore.com>

	* 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  <schonberg@adacore.com>

	* exp_ch5.adb: Code clean up.
	* sem_ch13.adb: Minor fix in comment.

2015-10-16  Bob Duff  <duff@adacore.com>

	* 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
This commit is contained in:
Arnaud Charlet 2015-10-16 15:43:47 +02:00
parent 7f37fff1a1
commit e1e307d941
8 changed files with 195 additions and 134 deletions

View File

@ -1,3 +1,27 @@
2015-10-16 Hristian Kirtchev <kirtchev@adacore.com>
* 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 <schonberg@adacore.com>
* exp_ch5.adb: Code clean up.
* sem_ch13.adb: Minor fix in comment.
2015-10-16 Bob Duff <duff@adacore.com>
* 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 <miranda@adacore.com>
* sem_ch5.adb (Analyze_Iterator_Specification): Associate a

View File

@ -152,8 +152,8 @@ package body Ada.Exceptions is
--
-- The format of the string is as follows:
--
-- Exception_Name: <exception name> (as in Exception_Name)
-- Message: <message> (only if Exception_Message is empty)
-- raised <exception name> : <message>
-- (" : <message>" 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)

View File

@ -117,8 +117,8 @@ package body Ada.Exceptions is
--
-- The format of the string is as follows:
--
-- Exception_Name: <exception name> (as in Exception_Name)
-- Message: <message> (only if Exception_Message is empty)
-- raised <exception name> : <message>
-- (" : <message>" 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)

View File

@ -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;

View File

@ -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
if S (From .. From + 6) /= "raised " then
Bad_EO;
end if;
declare
Name_Start : constant Positive := From + 7;
begin
From := Name_Start + 1;
while From < To and then S (From) /= ' ' loop
From := From + 1;
end loop;
X.Id :=
Exception_Id (Internal_Exception (S (Name_Start .. From - 1)));
end;
if From <= To then
if S (From .. From + 2) /= " : " then
Bad_EO;
end if;
X.Id := Exception_Id (Internal_Exception (S (From + 16 .. To)));
X.Msg_Length := To - From - 2;
X.Msg (1 .. X.Msg_Length) := S (From + 3 .. To);
else
X.Msg_Length := 0;
end if;
Next_String;
X.Pid := 0;
if From <= To and then S (From) = 'P' then
if S (From .. From + 3) /= "PID:" then
Bad_EO;
end if;
From := From + 5; -- skip past PID: space
while From <= To loop
X.Pid := X.Pid * 10 +
(Character'Pos (S (From)) - Character'Pos ('0'));
From := From + 1;
end loop;
Next_String;
if From <= To and then S (From) = 'M' then
if S (From .. From + 8) /= "Message: " then
Bad_EO;
end if;
X.Msg_Length := To - From - 8;
X.Msg (1 .. X.Msg_Length) := S (From + 9 .. To);
Next_String;
else
X.Msg_Length := 0;
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;
From := From + 5; -- skip past PID: space
while From <= To loop
X.Pid := X.Pid * 10 +
(Character'Pos (S (From)) - Character'Pos ('0'));
From := From + 1;
end loop;
Next_String;
end if;
X.Num_Tracebacks := 0;
if From <= To then
if S (From .. To) /= "Call stack traceback locations:" then
Bad_EO;
end if;
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;
C := 0;
while From <= To loop
Ch := S (From);
if Ch in '0' .. '9' then
N :=
Character'Pos (S (From)) - Character'Pos ('0');
elsif Ch in 'a' .. 'f' then
N :=
Character'Pos (S (From)) - Character'Pos ('a') + 10;
elsif Ch = ' ' then
From := From + 1;
exit;
else
Bad_EO;
end if;
C := C * 16 + N;
From := From + 1;
end loop;
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 if;
X.Num_Tracebacks := 0;
if From <= To then
if S (From .. To) /= "Call stack traceback locations:" then
Bad_EO;
end if;
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;
C := 0;
while From <= To loop
Ch := S (From);
if Ch in '0' .. '9' then
N :=
Character'Pos (S (From)) - Character'Pos ('0');
elsif Ch in 'a' .. 'f' then
N :=
Character'Pos (S (From)) - Character'Pos ('a') + 10;
elsif Ch = ' ' then
From := From + 1;
exit;
else
Bad_EO;
end if;
C := C * 16 + N;
From := From + 1;
end loop;
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;

View File

@ -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;

View File

@ -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);

View File

@ -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