+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
--
-- 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)
--
-- 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)
-- 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
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
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;
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;
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 :=
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;
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;
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;
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
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
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
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;
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,
end if;
Restore_Env;
+ Ignore_Pragma_SPARK_Mode := Saved_IPSM;
Style_Check := Saved_Style_Check;
Restore_Warnings (Saved_Warnings);
(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);
-- 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