+2017-11-16 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_elab.adb (Include): Including a node which is also a compilation
+ unit terminates the search because there are no more lists to examine.
+
+2017-11-16 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch8.adb (Analyze_Subprogram_Renaming): Ensure that a renaming
+ declaration does not define a primitive operation of a tagged type for
+ SPARK.
+ (Check_SPARK_Primitive_Operation): New routine.
+
+2017-11-16 Arnaud Charlet <charlet@adacore.com>
+
+ * libgnat/a-elchha.adb (Last_Chance_Handler): Display Argv (0) in
+ message when using -E binder switch.
+
+2017-11-16 Piotr Trojanek <trojanek@adacore.com>
+
+ * errout.ads: Fix minor typo in comment.
+
2017-11-16 Ed Schonberg <schonberg@adacore.com>
* sem_ch3.adb (Process_Subtype): If the subtype indication does not
-- Insertion character } (Right brace: insert type reference)
-- The character } is replaced by a string describing the type
-- referenced by the entity whose Id is stored in Error_Msg_Node_1.
- -- the string gives the name or description of the type, and also
+ -- The string gives the name or description of the type, and also
-- where appropriate the location of its declaration. Special cases
-- like "some integer type" are handled appropriately. Only one } is
-- allowed in a message, since there is not enough room for two (the
pragma Compiler_Unit_Warning;
with System.Standard_Library; use System.Standard_Library;
-with System.Soft_Links;
+with System.Soft_Links; use System;
procedure Ada.Exceptions.Last_Chance_Handler
(Except : Exception_Occurrence)
pragma Import (Ada, To_Stderr, "__gnat_to_stderr");
-- Little routine to output string to stderr
+ Gnat_Argv : System.Address;
+ pragma Import (C, Gnat_Argv, "gnat_argv");
+
+ procedure Fill_Arg (A : System.Address; Arg_Num : Integer);
+ pragma Import (C, Fill_Arg, "__gnat_fill_arg");
+
+ function Len_Arg (Arg_Num : Integer) return Integer;
+ pragma Import (C, Len_Arg, "__gnat_len_arg");
+
Ptr : Natural := 0;
Nobuf : String (1 .. 0);
else
To_Stderr (Nline);
- To_Stderr ("Execution terminated by unhandled exception");
+
+ if Gnat_Argv = System.Null_Address then
+ To_Stderr ("Execution terminated by unhandled exception");
+ else
+ declare
+ Arg : aliased String (1 .. Len_Arg (0));
+ begin
+ Fill_Arg (Arg'Address, 0);
+ To_Stderr ("Execution of ");
+ To_Stderr (Arg);
+ To_Stderr (" terminated by unhandled exception");
+ end;
+ end if;
+
To_Stderr (Nline);
Append_Info_Untailored_Exception_Information (Except, Nobuf, Ptr);
with Sem_Dist; use Sem_Dist;
with Sem_Elab; use Sem_Elab;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
with Sem_Type; use Sem_Type;
-- have one. Otherwise the subtype of Sub's return profile must
-- exclude null.
+ procedure Check_SPARK_Primitive_Operation (Subp_Id : Entity_Id);
+ -- Ensure that a SPARK renaming denoted by its entity Subp_Id does not
+ -- declare a primitive operation of a tagged type (SPARK RM 6.1.1(3)).
+
procedure Freeze_Actual_Profile;
-- In Ada 2012, enforce the freezing rule concerning formal incomplete
-- types: a callable entity freezes its profile, unless it has an
end if;
end Check_Null_Exclusion;
+ -------------------------------------
+ -- Check_SPARK_Primitive_Operation --
+ -------------------------------------
+
+ procedure Check_SPARK_Primitive_Operation (Subp_Id : Entity_Id) is
+ Prag : constant Node_Id := SPARK_Pragma (Subp_Id);
+ Typ : Entity_Id;
+
+ begin
+ -- Nothing to do when the subprogram appears within an instance
+
+ if In_Instance then
+ return;
+
+ -- Nothing to do when the subprogram is not subject to SPARK_Mode On
+ -- because this check applies to SPARK code only.
+
+ elsif not (Present (Prag)
+ and then Get_SPARK_Mode_From_Annotation (Prag) = On)
+ then
+ return;
+
+ -- Nothing to do when the subprogram is not a primitive operation
+
+ elsif not Is_Primitive (Subp_Id) then
+ return;
+ end if;
+
+ Typ := Find_Dispatching_Type (Subp_Id);
+
+ -- Nothing to do when the subprogram is a primitive operation of an
+ -- untagged type.
+
+ if No (Typ) then
+ return;
+ end if;
+
+ -- At this point a renaming declaration introduces a new primitive
+ -- operation for a tagged type.
+
+ Error_Msg_Node_2 := Typ;
+ Error_Msg_NE
+ ("subprogram renaming & cannot declare primitive for type & "
+ & "(SPARK RM 6.1.1(3))", N, Subp_Id);
+ end Check_SPARK_Primitive_Operation;
+
---------------------------
-- Freeze_Actual_Profile --
---------------------------
-- Set SPARK mode from current context
- Set_SPARK_Pragma (New_S, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma (New_S, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (New_S);
Rename_Spec := Find_Corresponding_Spec (N);
Generate_Definition (New_S);
New_Overloaded_Entity (New_S);
- if Is_Entity_Name (Nam)
- and then Is_Intrinsic_Subprogram (Entity (Nam))
+ if not (Is_Entity_Name (Nam)
+ and then Is_Intrinsic_Subprogram (Entity (Nam)))
then
- null;
- else
Check_Delayed_Subprogram (New_S);
end if;
+
+ -- Verify that a SPARK renaming does not declare a primitive
+ -- operation of a tagged type.
+
+ Check_SPARK_Primitive_Operation (New_S);
end if;
-- There is no need for elaboration checks on the new entity, which may
elsif Requires_Overriding (Old_S)
or else
- (Is_Abstract_Subprogram (Old_S)
- and then Present (Find_Dispatching_Type (Old_S))
- and then
- not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
+ (Is_Abstract_Subprogram (Old_S)
+ and then Present (Find_Dispatching_Type (Old_S))
+ and then not Is_Abstract_Type (Find_Dispatching_Type (Old_S)))
then
Error_Msg_N
("renamed entity cannot be subprogram that requires overriding "
procedure Include (N : Node_Id; Curr : in out Node_Id);
pragma Inline (Include);
-- Update the Curr and Start pointers to include arbitrary construct N
- -- in the early call region.
+ -- in the early call region. This routine raises ECR_Found.
function Is_OK_Preelaborable_Construct (N : Node_Id) return Boolean;
pragma Inline (Is_OK_Preelaborable_Construct);
procedure Include (N : Node_Id; Curr : in out Node_Id) is
begin
Start := N;
- Curr := Prev (Start);
+
+ -- The input node is a compilation unit. This terminates the search
+ -- because there are no more lists to inspect and there are no more
+ -- enclosing constructs to climb up to. The transitions are:
+ --
+ -- private declarations -> terminate
+ -- visible declarations -> terminate
+ -- statements -> terminate
+ -- declarations -> terminate
+
+ if Nkind (Parent (Start)) = N_Compilation_Unit then
+ raise ECR_Found;
+
+ -- Otherwise the input node is still within some list
+
+ else
+ Curr := Prev (Start);
+ end if;
end Include;
-----------------------------------
git://gcc.gnu.org / gcc.git / commitdiff