[multiple changes]

2014-01-24  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.adb (Is_Post_State): In a postcondition, a selected
	component that denotes an implicit dereference is a reference
	to the post state of the subprogram.

2014-01-24  Robert Dewar  <dewar@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode OFF
	for generated subprograms.
	(Analyze_Subprogram_Specification): Ditto.

2014-01-24  Vincent Celier  <celier@adacore.com>

	* prj-dect.adb (Check_Attribute_Allowed): Detect more forbidden
	attributes in package Builder of aggregate and aggregate library
	projects.
	* prj-nmsc.adb (Process_Naming_Scheme.Check.Check_Aggregate):
	Remove procedure (Process_Naming_Scheme.Check.Check_Aggregated):
	Remove parameters.  Change error message from "... externally
	build library ..." to "... externally built project ...".
	(Process_Naming_Scheme.Check): Do not do any check in aggregate
	project, as attribute Library_Dir and Library_Name have already
	been detected as forbidden.

2014-01-24  Vincent Celier  <celier@adacore.com>

	* prj-env.adb (Find_Project): If cached project path is not in
	project directory, look in current directory first and use cached
	project path only if project is not found in project directory.

From-SVN: r207032

6 files changed, 139 insertions, 98 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cabedee..8c6087a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,34 @@
+2014-01-24  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_util.adb (Is_Post_State): In a postcondition, a selected
+	component that denotes an implicit dereference is a reference
+	to the post state of the subprogram.
+
+2014-01-24  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode OFF
+	for generated subprograms.
+	(Analyze_Subprogram_Specification): Ditto.
+
+2014-01-24  Vincent Celier  <celier@adacore.com>
+
+	* prj-dect.adb (Check_Attribute_Allowed): Detect more forbidden
+	attributes in package Builder of aggregate and aggregate library
+	projects.
+	* prj-nmsc.adb (Process_Naming_Scheme.Check.Check_Aggregate):
+	Remove procedure (Process_Naming_Scheme.Check.Check_Aggregated):
+	Remove parameters.  Change error message from "... externally
+	build library ..." to "... externally built project ...".
+	(Process_Naming_Scheme.Check): Do not do any check in aggregate
+	project, as attribute Library_Dir and Library_Name have already
+	been detected as forbidden.
+
+2014-01-24  Vincent Celier  <celier@adacore.com>
+
+	* prj-env.adb (Find_Project): If cached project path is not in
+	project directory, look in current directory first and use cached
+	project path only if project is not found in project directory.
+
 2014-01-24  Robert Dewar  <dewar@adacore.com>
 
 	* sem_util.adb, lib-xref.adb: Correct false positive warnings.
diff --git a/gcc/ada/prj-dect.adb b/gcc/ada/prj-dect.adb
index b1a1738..2ce0310 100644
--- a/gcc/ada/prj-dect.adb
+++ b/gcc/ada/prj-dect.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2001-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 2001-2013, 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- --
@@ -253,6 +253,16 @@ package body Prj.Dect is
               or else Name = Snames.Name_Exec_Dir
               or else Name = Snames.Name_Source_Dirs
               or else Name = Snames.Name_Inherit_Source_Path
+              or else
+                (Qualif = Aggregate and then Name = Snames.Name_Library_Dir)
+              or else
+                (Qualif = Aggregate and then Name = Snames.Name_Library_Name)
+              or else Name = Snames.Name_Main
+              or else Name = Snames.Name_Roots
+              or else Name = Snames.Name_Externally_Built
+              or else Name = Snames.Name_Executable
+              or else Name = Snames.Name_Executable_Suffix
+              or else Name = Snames.Name_Default_Switches
             then
                Error_Msg_Name_1 := Name;
                Error_Msg
diff --git a/gcc/ada/prj-env.adb b/gcc/ada/prj-env.adb
index 67b077f..7943672 100644
--- a/gcc/ada/prj-env.adb
+++ b/gcc/ada/prj-env.adb
@@ -2229,19 +2229,20 @@ package body Prj.Env is
       Directory          : String;
       Path               : out Namet.Path_Name_Type)
    is
+      Result  : String_Access;
+      Has_Dot : Boolean := False;
+      Key     : Name_Id;
+
       File : constant String := Project_File_Name;
       --  Have to do a copy, in case the parameter is Name_Buffer, which we
-      --  modify below
+      --  modify below.
 
-      function Try_Path_Name is new Find_Name_In_Path
-        (Check_Filename => Is_Regular_File);
-      --  Find a file in the project search path
-
-      --  Local Declarations
+      Cached_Path : Namet.Path_Name_Type;
+      --  This should be commented rather than making us guess from the name???
 
-      Result  : String_Access;
-      Has_Dot : Boolean := False;
-      Key     : Name_Id;
+      function Try_Path_Name is new
+        Find_Name_In_Path (Check_Filename => Is_Regular_File);
+      --  Find a file in the project search path
 
    --  Start of processing for Find_Project
 
@@ -2259,12 +2260,7 @@ package body Prj.Env is
       Name_Len := File'Length;
       Name_Buffer (1 .. Name_Len) := File;
       Key := Name_Find;
-      Path := Projects_Paths.Get (Self.Cache, Key);
-
-      if Path /= No_Path then
-         Debug_Decrease_Indent;
-         return;
-      end if;
+      Cached_Path := Projects_Paths.Get (Self.Cache, Key);
 
       --  Check if File contains an extension (a dot before a
       --  directory separator). If it is the case we do not try project file
@@ -2283,13 +2279,42 @@ package body Prj.Env is
 
       if not Is_Absolute_Path (File) then
 
+         --  If we have found project in the cache, check if in the directory
+
+         if Cached_Path /= No_Path then
+            declare
+               Cached : constant String := Get_Name_String (Cached_Path);
+            begin
+               if (not Has_Dot
+                    and then Cached =
+                      GNAT.OS_Lib.Normalize_Pathname
+                        (File & Project_File_Extension,
+                         Directory      => Directory,
+                         Resolve_Links  => Opt.Follow_Links_For_Files,
+                         Case_Sensitive => True))
+                 or else
+                   Cached =
+                     GNAT.OS_Lib.Normalize_Pathname
+                       (File,
+                        Directory      => Directory,
+                        Resolve_Links  => Opt.Follow_Links_For_Files,
+                        Case_Sensitive => True)
+               then
+                  Path := Cached_Path;
+                  Debug_Decrease_Indent;
+                  return;
+               end if;
+            end;
+         end if;
+
          --  First we try <directory>/<file_name>.<extension>
 
          if not Has_Dot then
-            Result := Try_Path_Name
-              (Self,
-               Directory & Directory_Separator &
-               File & Project_File_Extension);
+            Result :=
+              Try_Path_Name
+                (Self,
+                 Directory & Directory_Separator &
+                   File & Project_File_Extension);
          end if;
 
          --  Then we try <directory>/<file_name>
@@ -2300,6 +2325,14 @@ package body Prj.Env is
          end if;
       end if;
 
+      --  If we found the path in the cache, this is the one
+
+      if Result = null and then Cached_Path /= No_Path then
+         Path := Cached_Path;
+         Debug_Decrease_Indent;
+         return;
+      end if;
+
       --  Then we try <file_name>.<extension>
 
       if Result = null and then not Has_Dot then
diff --git a/gcc/ada/prj-nmsc.adb b/gcc/ada/prj-nmsc.adb
index eb647df..54c4e4e 100644
--- a/gcc/ada/prj-nmsc.adb
+++ b/gcc/ada/prj-nmsc.adb
@@ -8395,71 +8395,14 @@ package body Prj.Nmsc is
          In_Aggregate_Lib : Boolean;
          Data             : in out Tree_Processing_Data)
       is
-         procedure Check_Aggregate
-           (Project : Project_Id;
-            Data    : in out Tree_Processing_Data);
-         --  Check the aggregate project attributes, reject any not supported
-         --  attributes.
-
-         procedure Check_Aggregated
-           (Project : Project_Id;
-            Data    : in out Tree_Processing_Data);
-         --  Check aggregated projects which should not be externally built.
-         --  What is Data??? if same as outer Data, why passed???
-         --  What exact check is performed here??? Seems a bad idea to have
-         --  two procedures with such close names ???
-
-         ---------------------
-         -- Check_Aggregate --
-         ---------------------
-
-         procedure Check_Aggregate
-           (Project : Project_Id;
-            Data    : in out Tree_Processing_Data)
-         is
-            procedure Check_Not_Defined (Name : Name_Id);
-            --  Report an error if Var is defined
-
-            -----------------------
-            -- Check_Not_Defined --
-            -----------------------
-
-            procedure Check_Not_Defined (Name : Name_Id) is
-               Var : constant Prj.Variable_Value :=
-                       Prj.Util.Value_Of
-                         (Name, Project.Decl.Attributes, Data.Tree.Shared);
-            begin
-               if not Var.Default then
-                  Error_Msg_Name_1 := Name;
-                  Error_Msg
-                    (Data.Flags, "wrong attribute %% in aggregate library",
-                     Var.Location, Project);
-               end if;
-            end Check_Not_Defined;
-
-         --  Start of processing for Check_Aggregate
-
-         begin
-            Check_Not_Defined (Snames.Name_Library_Dir);
-            Check_Not_Defined (Snames.Name_Library_Interface);
-            Check_Not_Defined (Snames.Name_Library_Name);
-            Check_Not_Defined (Snames.Name_Library_Ali_Dir);
-            Check_Not_Defined (Snames.Name_Library_Src_Dir);
-            Check_Not_Defined (Snames.Name_Library_Options);
-            Check_Not_Defined (Snames.Name_Library_Standalone);
-            Check_Not_Defined (Snames.Name_Library_Kind);
-            Check_Not_Defined (Snames.Name_Leading_Library_Options);
-            Check_Not_Defined (Snames.Name_Library_Version);
-         end Check_Aggregate;
+         procedure Check_Aggregated;
+         --  Check aggregated projects which should not be externally built
 
          ----------------------
          -- Check_Aggregated --
          ----------------------
 
-         procedure Check_Aggregated
-           (Project : Project_Id;
-            Data    : in out Tree_Processing_Data)
-         is
+         procedure Check_Aggregated is
             L : Aggregated_Project_List;
 
          begin
@@ -8478,7 +8421,7 @@ package body Prj.Nmsc is
                      Error_Msg_Name_1 := L.Project.Display_Name;
                      Error_Msg
                        (Data.Flags,
-                        "cannot aggregate externally build library %%",
+                        "cannot aggregate externally built project %%",
                         Var.Location, Project);
                   end if;
                end;
@@ -8504,10 +8447,10 @@ package body Prj.Nmsc is
 
          case Project.Qualifier is
             when Aggregate =>
-               Check_Aggregated (Project, Data);
+               Check_Aggregated;
 
             when Aggregate_Library =>
-               Check_Aggregated (Project, Data);
+               Check_Aggregated;
 
                if Project.Object_Directory = No_Path_Information then
                   Project.Object_Directory := Project.Directory;
@@ -8532,12 +8475,7 @@ package body Prj.Nmsc is
 
          Check_Configuration (Project, Data);
 
-         --  For aggregate project check no library attributes are defined
-
-         if Project.Qualifier = Aggregate then
-            Check_Aggregate (Project, Data);
-
-         else
+         if Project.Qualifier /= Aggregate then
             Check_Library_Attributes (Project, Data);
             Check_Package_Naming (Project, Data);
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index f46f2e9..3fa6183 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2995,9 +2995,17 @@ package body Sem_Ch6 is
 
             Push_Scope (Spec_Id);
 
-            --  Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
+            --  Set SPARK_Mode
 
-            if Present (SPARK_Pragma (Spec_Id))
+            --  For internally generated subprogram, always off
+
+            if not Comes_From_Source (Spec_Id) then
+               SPARK_Mode := Off;
+               SPARK_Mode_Pragma := Empty;
+
+            --  Inherited from spec
+
+            elsif Present (SPARK_Pragma (Spec_Id))
               and then not SPARK_Pragma_Inherited (Spec_Id)
             then
                SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
@@ -3058,12 +3066,19 @@ package body Sem_Ch6 is
               (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True);
             Install_Formals (Body_Id);
 
-            --  Set SPARK_Mode from context
+            Push_Scope (Body_Id);
 
-            Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
-            Set_SPARK_Pragma_Inherited (Body_Id, True);
+            --  Set SPARK_Mode from context or OFF for internal routine
 
-            Push_Scope (Body_Id);
+            if Comes_From_Source (Body_Id) then
+               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
+            else
+               Set_SPARK_Pragma (Body_Id, Empty);
+               Set_SPARK_Pragma_Inherited (Body_Id, False);
+               SPARK_Mode := Off;
+               SPARK_Mode_Pragma := Empty;
+            end if;
          end if;
 
          --  For stubs and bodies with no previous spec, generate references to
@@ -3609,8 +3624,16 @@ package body Sem_Ch6 is
 
       Generate_Definition (Designator);
 
-      Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
-      Set_SPARK_Pragma_Inherited (Designator, True);
+      --  Set SPARK mode, always off for internal routines, otherwise set
+      --  from current context (may be overwritten later with explicit pragma)
+
+      if Comes_From_Source (Designator) then
+         Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Designator, True);
+      else
+         Set_SPARK_Pragma (Designator, Empty);
+         Set_SPARK_Pragma_Inherited (Designator, False);
+      end if;
 
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 422e462..cf00b2f 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2618,7 +2618,13 @@ package body Sem_Util is
             elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
                Ent := Entity (N);
 
-               if No (Ent) or else Ekind (Ent) in Assignable_Kind then
+               --  The entity may be modifiable through an implicit dereference
+
+               if No (Ent)
+                 or else Ekind (Ent) in Assignable_Kind
+                 or else (Is_Access_Type (Etype (Ent))
+                           and then Nkind (Parent (N)) = N_Selected_Component)
+               then
                   Post_State_Seen := True;
                   return Abandon;
                end if;