+2016-06-20 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * make.adb, gnatbind.adb, g-socket.adb, sem_ch13.adb: Minor
+ reformatting.
+ * lib.ads, sem_util.adb: Minor typo in comment.
+
+2016-06-20 Yannick Moy <moy@adacore.com>
+
+ * sem_prag.adb, sem_prag.ads (Build_Pragma_Check_Equivalent):
+ Add parameter Keep_Pragma_Id to optionally keep
+ the identifier of the pragma instead of converting
+ to pragma Check. Also set type of new function call
+ appropriately. (Collect_Inherited_Class_Wide_Conditions):
+ Call Build_Pragma_Check_Equivalent with the new parameter
+ Keep_Pragma_Id set to True to keep the identifier of the copied
+ pragma.
+ * sinfo.ads: Add comment.
+
+2016-06-20 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch7.adb (Build_Invariant_Procedure_Body):
+ Always install the scope of the invariant procedure
+ in order to produce better error messages. Do not
+ insert the body when the context is a generic unit.
+ (Build_Invariant_Procedure_Declaration): Perform minimal
+ decoration of the invariant procedure and its formal parameter
+ in case they are not analyzed. Do not insert the declaration
+ when the context is a generic unit.
+
2016-06-20 Ed Schonberg <schonberg@adacore.com>
* sem_ch13.adb (Visible_Component): New procedure, subsidiary
Set_Ghost_Mode_From_Entity (Work_Typ);
+ -- Emulate the environment of the invariant procedure by installing
+ -- its scope and formal parameters. Note that this is not need, but
+ -- having the scope of the invariant procedure installed helps with
+ -- the detection of invariant-related errors.
+
+ Push_Scope (Proc_Id);
+ Install_Formals (Proc_Id);
+
Obj_Id := First_Formal (Proc_Id);
+ pragma Assert (Present (Obj_Id));
-- The "partial" invariant procedure verifies the invariants of the
-- partial view only.
pragma Assert (Present (Priv_Typ));
Freeze_Typ := Priv_Typ;
- -- Emulate the environment of the invariant procedure by installing
- -- its scope and formal parameters. Note that this is not need, but
- -- having the scope of the invariant procedure installed helps with
- -- the detection of invariant-related errors.
-
- Push_Scope (Proc_Id);
- Install_Formals (Proc_Id);
-
Add_Type_Invariants
(Priv_Typ => Priv_Typ,
Full_Typ => Empty,
Obj_Id => Obj_Id,
Checks => Stmts);
- End_Scope;
-
-- Otherwise the "full" invariant procedure verifies the invariants of
-- the full view, all array or record components, as well as class-wide
-- invariants inherited from parent types or interfaces. In addition, it
Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
end if;
+ End_Scope;
+
-- At this point there should be at least one invariant check. If this
-- is not the case, then the invariant-related flags were not properly
-- set, or there is a missing invariant procedure on one of the array
Stmts := New_List (Make_Null_Statement (Loc));
end if;
+ -- Generate:
+ -- procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>) is
+ -- begin
+ -- <Stmts>
+ -- end <Work_Typ>[Partial_]Invariant;
+
Proc_Body :=
Make_Subprogram_Body (Loc,
Specification =>
Statements => Stmts));
Proc_Body_Id := Defining_Entity (Proc_Body);
+ -- Perform minor decoration in case the body is not analyzed
+
Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
Set_Etype (Proc_Body_Id, Standard_Void_Type);
- Set_Scope (Proc_Body_Id, Scope (Typ));
+ Set_Scope (Proc_Body_Id, Current_Scope);
-- Link both spec and body to avoid generating duplicates
Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
Set_Corresponding_Spec (Proc_Body, Proc_Id);
- Append_Freeze_Action (Freeze_Typ, Proc_Body);
+ -- The body should not be inserted into the tree when the context is a
+ -- generic unit because it is not part of the template. Note that the
+ -- body must still be generated in order to resolve the invariants.
+
+ if Inside_A_Generic then
+ null;
+
+ -- Otherwise the body is part of the freezing actions of the type
+
+ else
+ Append_Freeze_Action (Freeze_Typ, Proc_Body);
+ end if;
+
Ghost_Mode := Save_Ghost_Mode;
end Build_Invariant_Procedure_Body;
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
- Proc_Id : Entity_Id;
- Typ_Decl : Node_Id;
+ Proc_Decl : Node_Id;
+ Proc_Id : Entity_Id;
+ Proc_Nam : Name_Id;
+ Typ_Decl : Node_Id;
CRec_Typ : Entity_Id;
-- The corresponding record type of Full_Typ
-- procedure.
if Partial_Invariant then
- Proc_Id :=
- Make_Defining_Identifier (Loc,
- Chars =>
- New_External_Name (Chars (Work_Typ), "Partial_Invariant"));
-
- Set_Ekind (Proc_Id, E_Procedure);
- Set_Is_Partial_Invariant_Procedure (Proc_Id);
- Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+ Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant");
-- Otherwise the caller requests the declaration of the "full" invariant
-- procedure.
else
- Proc_Id :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Work_Typ), "Invariant"));
+ Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant");
+ end if;
+
+ Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam);
+
+ -- Perform minor decoration in case the declaration is not analyzed
- Set_Ekind (Proc_Id, E_Procedure);
+ Set_Ekind (Proc_Id, E_Procedure);
+ Set_Etype (Proc_Id, Standard_Void_Type);
+ Set_Scope (Proc_Id, Current_Scope);
+
+ if Partial_Invariant then
+ Set_Is_Partial_Invariant_Procedure (Proc_Id);
+ Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id);
+ else
Set_Is_Invariant_Procedure (Proc_Id);
Set_Invariant_Procedure (Work_Typ, Proc_Id);
end if;
-- of the current type instance.
Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
+
+ -- Perform minor decoration in case the declaration is not analyzed
+
Set_Ekind (Obj_Id, E_In_Parameter);
+ Set_Etype (Obj_Id, Work_Typ);
+ Set_Scope (Obj_Id, Proc_Id);
+
+ Set_First_Entity (Proc_Id, Obj_Id);
-- Generate:
-- procedure <Work_Typ>[Partial_]Invariant (_object : <Work_Typ>);
- Insert_After_And_Analyze (Typ_Decl,
+ Proc_Decl :=
Make_Subprogram_Declaration (Loc,
Specification =>
Make_Procedure_Specification (Loc,
Make_Parameter_Specification (Loc,
Defining_Identifier => Obj_Id,
Parameter_Type =>
- New_Occurrence_Of (Work_Typ, Loc))))));
+ New_Occurrence_Of (Work_Typ, Loc)))));
+
+ -- The declaration should not be inserted into the tree when the context
+ -- is a generic unit because it is not part of the template.
+
+ if Inside_A_Generic then
+ null;
+
+ -- Otherwise insert the declaration
+
+ else
+ pragma Assert (Present (Typ_Decl));
+ Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
+ end if;
Ghost_Mode := Save_Ghost_Mode;
end Build_Invariant_Procedure_Declaration;
function Is_IP_Address (Name : String) return Boolean is
Dots : Natural := 0;
+
begin
- -- Perform a cursory check for a dotted quad: we must have 1 to 3
- -- dots, and there must be at least one digit around each.
+ -- Perform a cursory check for a dotted quad: we must have 1 to 3 dots,
+ -- and there must be at least one digit around each.
for J in Name'Range loop
if Name (J) = '.' then
- -- Check that the dot is not in first or last position, and
- -- that it is followed by a digit. Note that we already know
- -- that it is preceded by a digit, or we would have returned
- -- earlier on.
+ -- Check that the dot is not in first or last position, and that
+ -- it is followed by a digit. Note that we already know that it is
+ -- preceded by a digit, or we would have returned earlier on.
if J in Name'First + 1 .. Name'Last - 1
and then Name (J + 1) in '0' .. '9'
then
Dots := Dots + 1;
- else
-
- -- Definitely not a proper dotted quad
+ -- Definitely not a proper dotted quad
+ else
return False;
end if;
-- only with switch -R.
procedure Add_Artificial_ALI_File (Name : String);
- -- Artificially add ALI file Name in the closure.
+ -- Artificially add ALI file Name in the closure
function Gnatbind_Supports_Auto_Init return Boolean;
-- Indicates if automatic initialization of elaboration procedure
procedure Add_Artificial_ALI_File (Name : String) is
Id : ALI_Id;
pragma Warnings (Off, Id);
+
begin
Name_Len := Name'Length;
Name_Buffer (1 .. Name_Len) := Name;
-----------------
-- The units table has an entry for each unit (source file) read in by the
- -- current compilation. The table is indexed by the unit number value,
+ -- current compilation. The table is indexed by the unit number value.
-- The first entry in the table, subscript Main_Unit, is for the main file.
-- Each entry in this units table contains the following data.
-- Dynamic_Elab
-- A flag indicating if this unit was compiled with dynamic elaboration
-- checks specified (as the result of using the -gnatE compilation
- -- option or a pragma Elaboration_Checks (Dynamic).
+ -- option or a pragma Elaboration_Checks (Dynamic)).
-- Error_Location
-- This is copied from the Sloc field of the Enode argument passed
procedure Check_Standard_Library is
begin
Need_To_Check_Standard_Library := False;
-
Name_Len := 0;
if not Targparm.Suppress_Standard_Library_On_Target then
end if;
declare
- Sfile : File_Name_Type;
Add_It : Boolean := True;
+ Sfile : File_Name_Type;
begin
Sfile := Name_Enter;
function Replace_Type_Ref (N : Node_Id) return Traverse_Result is
Loc : constant Source_Ptr := Sloc (N);
- C : Entity_Id;
- S : Entity_Id;
- P : Node_Id;
procedure Add_Prefix (Ref : Node_Id; Comp : Entity_Id);
- -- Add the proper prefix to a reference to a component of the
- -- type when it is not already a selected component.
+ -- Add the proper prefix to a reference to a component of the type
+ -- when it is not already a selected component.
----------------
-- Add_Prefix --
begin
Rewrite (Ref,
Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (T, Loc),
+ Prefix => New_Occurrence_Of (T, Loc),
Selector_Name => New_Occurrence_Of (Comp, Loc)));
Replace_Type_Reference (Prefix (Ref));
end Add_Prefix;
+ -- Local variables
+
+ Comp : Entity_Id;
+ Pref : Node_Id;
+ Scop : Entity_Id;
+
-- Start of processing for Replace_Type_Ref
begin
elsif Nkind (Parent (N)) = N_Indexed_Component
and then N = Prefix (Parent (N))
then
- C := Visible_Component (Chars (N));
+ Comp := Visible_Component (Chars (N));
- if Present (C) and then Is_Array_Type (Etype (C)) then
- Add_Prefix (N, C);
+ if Present (Comp) and then Is_Array_Type (Etype (Comp)) then
+ Add_Prefix (N, Comp);
end if;
else
- C := Visible_Component (Chars (N));
+ Comp := Visible_Component (Chars (N));
- if Present (C) then
- Add_Prefix (N, C);
+ if Present (Comp) then
+ Add_Prefix (N, Comp);
end if;
end if;
else
-- Loop through scopes and prefixes, doing comparison
- S := Current_Scope;
- P := Prefix (N);
+ Scop := Current_Scope;
+ Pref := Prefix (N);
loop
-- Continue if no more scopes or scope with no name
- if No (S) or else Nkind (S) not in N_Has_Chars then
+ if No (Scop) or else Nkind (Scop) not in N_Has_Chars then
return OK;
end if;
-- Do replace if prefix is an identifier matching the scope
-- that we are currently looking at.
- if Nkind (P) = N_Identifier
- and then Chars (P) = Chars (S)
+ if Nkind (Pref) = N_Identifier
+ and then Chars (Pref) = Chars (Scop)
then
Replace_Type_Reference (N);
return Skip;
-- of a selected component, whose selector matches the scope
-- we are currently looking at.
- if Nkind (P) = N_Selected_Component
- and then Nkind (Selector_Name (P)) = N_Identifier
- and then Chars (Selector_Name (P)) = Chars (S)
+ if Nkind (Pref) = N_Selected_Component
+ and then Nkind (Selector_Name (Pref)) = N_Identifier
+ and then Chars (Selector_Name (Pref)) = Chars (Scop)
then
- S := Scope (S);
- P := Prefix (P);
+ Scop := Scope (Scop);
+ Pref := Prefix (Pref);
-- For anything else, we don't have a match, so keep on
-- going, there are still some weird cases where we may
end if;
end Replace_Type_Ref;
+ procedure Replace_Type_Refs is new Traverse_Proc (Replace_Type_Ref);
+
-----------------------
-- Visible_Component --
-----------------------
function Visible_Component (Comp : Name_Id) return Entity_Id is
E : Entity_Id;
+
begin
if Ekind (T) /= E_Record_Type then
return Empty;
else
E := First_Entity (T);
while Present (E) loop
- if Comes_From_Source (E)
- and then Chars (E) = Comp
- then
+ if Comes_From_Source (E) and then Chars (E) = Comp then
return E;
end if;
end if;
end Visible_Component;
- procedure Replace_Type_Refs is new Traverse_Proc (Replace_Type_Ref);
+ -- Start of processing for Replace_Type_References_Generic
begin
Replace_Type_Refs (N);
-----------------------------------
function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty;
+ Keep_Pragma_Id : Boolean := False) return Node_Id
is
Map : Elist_Id;
-- List containing the following mappings
& "for&#", N, Current_Scope);
end if;
+ -- Update type of function call node, which should be the same as
+ -- the function's return type.
+
+ if Is_Subprogram (Entity (N))
+ and then Nkind (Parent (N)) = N_Function_Call
+ then
+ Set_Etype (Parent (N), Etype (Entity (N)));
+ end if;
+
-- The whole expression will be reanalyzed
elsif Nkind (N) in N_Has_Etype then
Set_Analyzed (Check_Prag, False);
Set_Comes_From_Source (Check_Prag, False);
- Set_Class_Present (Check_Prag, False);
-- The tree of the original pragma may contain references to the
-- formal parameters of the related subprogram. At the same time
Nam := Prag_Nam;
end if;
- -- Convert the copy into pragma Check by correcting the name and adding
- -- a check_kind argument.
+ -- Unless Keep_Pragma_Id is True in order to keep the identifier of
+ -- the copied pragma in the newly created pragma, convert the copy into
+ -- pragma Check by correcting the name and adding a check_kind argument.
- Set_Pragma_Identifier
- (Check_Prag, Make_Identifier (Loc, Name_Check));
+ if not Keep_Pragma_Id then
+ Set_Class_Present (Check_Prag, False);
- Prepend_To (Pragma_Argument_Associations (Check_Prag),
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Nam)));
+ Set_Pragma_Identifier
+ (Check_Prag, Make_Identifier (Loc, Name_Check));
+
+ Prepend_To (Pragma_Argument_Associations (Check_Prag),
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Nam)));
+ end if;
-- Update the error message when the pragma is inherited
end if;
New_Prag :=
- Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp);
+ Build_Pragma_Check_Equivalent (Prag, Subp, Parent_Subp,
+ Keep_Pragma_Id => True);
Insert_After (Unit_Declaration_Node (Subp), New_Prag);
Preanalyze (New_Prag);
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- Perform preanalysis of pragma Test_Case
function Build_Pragma_Check_Equivalent
- (Prag : Node_Id;
- Subp_Id : Entity_Id := Empty;
- Inher_Id : Entity_Id := Empty) return Node_Id;
- -- Transform a [refined] pre- or postcondition denoted by Prag into an
+ (Prag : Node_Id;
+ Subp_Id : Entity_Id := Empty;
+ Inher_Id : Entity_Id := Empty;
+ Keep_Pragma_Id : Boolean := False) return Node_Id;
+ -- Transform a pre- or [refined] postcondition denoted by Prag into an
-- equivalent pragma Check. When the pre- or postcondition is inherited,
- -- the routine replaces the references of all formals of Inher_Id and
- -- primitive operations of its controlling type by references to the
- -- corresponding entities of Subp_Id and the descendant type.
+ -- the routine replaces the references of all formals of Inher_Id
+ -- and primitive operations of its controlling type by references
+ -- to the corresponding entities of Subp_Id and the descendant type.
+ -- Keep_Pragma_Id is True when the newly created pragma should be
+ -- in fact of the same kind as the source pragma Prag. This is used
+ -- in GNATprove_Mode to generate the inherited pre- and postconditions.
procedure Check_Applicable_Policy (N : Node_Id);
-- N is either an N_Aspect or an N_Pragma node. There are two cases. If
return True;
-- An array type is effectively volatile when it is subject to pragma
- -- Atomic_Components or Volatile_Components or its compolent type is
+ -- Atomic_Components or Volatile_Components or its component type is
-- effectively volatile.
elsif Is_Array_Type (Id) then
-- source, or because a Pre (resp. Post) aspect specification has been
-- broken into AND THEN sections. See Split_PPC for details.
+ -- In GNATprove mode, the inherited classwide pre- and postconditions
+ -- (suitably specialized for the specific type of the overriding
+ -- operation) are also in this list.
+
-- Contract_Test_Cases contains a collection of pragmas that correspond
-- to aspects/pragmas Contract_Cases and Test_Case. The ordering in the
-- list is in LIFO fashion.