2014-11-20 Robert Dewar <dewar@adacore.com>

	* a-stream.ads, a-reatim.ads, a-calend.ads, sinfo.ads, s-crtl.ads,
	interfac.ads, s-taskin.ads: Minor reformatting.

2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Extensions_Visible can now
	apply to an expression function.
	* sem_util.adb (Extensions_Visible_Status): Add special processing
	for expression functions.

2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* inline.adb (Build_Body_To_Inline): Remove meaningless aspects
	and pragmas.
	(Generate_Subprogram_Body): Remove meaningless aspects and pragmas.
	(Remove_Aspects_And_Pragmas): New routine.
	(Remove_Pragmas): Removed.
	* namet.ads, namet.adb (Nam_In): New versions of the routine.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@217841 138bc75d-0d04-0410-961f-82ee72b054a4

13 files changed, 366 insertions, 82 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b88ce84ee58..e43c701f2eb 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,24 @@
+2014-11-20  Robert Dewar  <dewar@adacore.com>
+
+	* a-stream.ads, a-reatim.ads, a-calend.ads, sinfo.ads, s-crtl.ads,
+	interfac.ads, s-taskin.ads: Minor reformatting.
+
+2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Extensions_Visible can now
+	apply to an expression function.
+	* sem_util.adb (Extensions_Visible_Status): Add special processing
+	for expression functions.
+
+2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* inline.adb (Build_Body_To_Inline): Remove meaningless aspects
+	and pragmas.
+	(Generate_Subprogram_Body): Remove meaningless aspects and pragmas.
+	(Remove_Aspects_And_Pragmas): New routine.
+	(Remove_Pragmas): Removed.
+	* namet.ads, namet.adb (Nam_In): New versions of the routine.
+
 2014-11-20  Thomas Quinot  <quinot@adacore.com>
 
 	* sem_util.adb: Minor reformatting.
diff --git a/gcc/ada/a-calend.ads b/gcc/ada/a-calend.ads
index 8e268b9c2b5..55efe115f5d 100644
--- a/gcc/ada/a-calend.ads
+++ b/gcc/ada/a-calend.ads
@@ -200,11 +200,15 @@ private
    type Time_Rep is new Long_Long_Integer;
    type Time is new Time_Rep;
    --  The underlying type of Time has been chosen to be a 64 bit signed
-   --  integer number since it allows for easier processing of sub seconds
+   --  integer number since it allows for easier processing of sub-seconds
    --  and arithmetic. We use Long_Long_Integer to allow this unit to compile
    --  when using custom target configuration files where the max integer is
-   --  32bits. This is useful for static analysis tools such as SPARK or
+   --  32 bits. This is useful for static analysis tools such as SPARK or
    --  CodePeer.
+   --
+   --  Note: the reason we have two separate types here is to avoid problems
+   --  with overloading ambiguities in the body if we tried to use Time as an
+   --  internal computational type.
 
    Days_In_Month : constant array (Month_Number) of Day_Number :=
                      (31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31);
diff --git a/gcc/ada/a-reatim.ads b/gcc/ada/a-reatim.ads
index b020adcd077..8558d460a58 100644
--- a/gcc/ada/a-reatim.ads
+++ b/gcc/ada/a-reatim.ads
@@ -90,12 +90,14 @@ package Ada.Real_Time is
    function Minutes (M : Integer) return Time_Span;
    pragma Ada_05 (Minutes);
 
-   --  Seconds_Count needs 64 bits, since Time has the full range of Duration.
-   --  The delta of Duration is 10 ** (-9), so the maximum number of seconds is
-   --  2**63/10**9 = 8*10**9 which does not quite fit in 32 bits.
-
-   type Seconds_Count is range
-     Long_Long_Integer'First .. Long_Long_Integer'Last;
+   type Seconds_Count is new Long_Long_Integer;
+   --  Seconds_Count needs 64 bits, since Time has the full range of
+   --  Duration. The delta of Duration is 10 ** (-9), so the maximum number of
+   --  seconds is 2**63/10**9 = 8*10**9 which does not quite fit in 32 bits.
+   --  However, rather than make this explicitly 64-bits we derive from
+   --  Long_Long_Integer. In normal usage this will have the same effect.
+   --  But in the case of CodePeer with a target configuration file with a
+   --  maximum integer size of 32, it allows analysis of this unit.
 
    procedure Split (T : Time; SC : out Seconds_Count; TS : out Time_Span);
    function Time_Of (SC : Seconds_Count; TS : Time_Span) return Time;
diff --git a/gcc/ada/a-stream.ads b/gcc/ada/a-stream.ads
index 0977f285f6f..40e60ce2499 100644
--- a/gcc/ada/a-stream.ads
+++ b/gcc/ada/a-stream.ads
@@ -41,8 +41,12 @@ package Ada.Streams is
 
    type Stream_Element is mod 2 ** Standard'Storage_Unit;
 
-   type Stream_Element_Offset is range
-      Long_Long_Integer'First .. Long_Long_Integer'Last;
+   type Stream_Element_Offset is new Long_Long_Integer;
+   --  Stream_Element_Offset needs 64 bits to accomodate large stream files.
+   --  However, rather than make this explicitly 64-bits we derive from
+   --  Long_Long_Integer. In normal usage this will have the same effect.
+   --  But in the case of CodePeer with a target configuration file with a
+   --  maximum integer size of 32, it allows analysis of this unit.
 
    subtype Stream_Element_Count is
       Stream_Element_Offset range 0 .. Stream_Element_Offset'Last;
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index c900cd394f3..9e97e8305fe 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -23,6 +23,7 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Debug;    use Debug;
 with Einfo;    use Einfo;
@@ -212,11 +213,21 @@ package body Inline is
    --  function anyway. This is also the case if the function is defined in a
    --  task body or within an entry (for example, an initialization procedure).
 
-   procedure Remove_Pragmas (Bod : Node_Id);
-   --  A pragma Unreferenced or pragma Unmodified that mentions a formal
-   --  parameter has no meaning when the body is inlined and the formals
-   --  are rewritten. Remove it from body to inline. The analysis of the
-   --  non-inlined body will handle the pragma properly.
+   procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id);
+   --  Remove all aspects and/or pragmas that have no meaning in inlined body
+   --  Body_Decl. The analysis of these items is performed on the non-inlined
+   --  body. The items currently removed are:
+   --    Contract_Cases
+   --    Global
+   --    Depends
+   --    Postcondition
+   --    Precondition
+   --    Refined_Global
+   --    Refined_Depends
+   --    Refined_Post
+   --    Test_Case
+   --    Unmodified
+   --    Unreferenced
 
    ------------------------------
    -- Deferred Cleanup Actions --
@@ -1103,12 +1114,12 @@ package body Inline is
       Set_Parameter_Specifications (Specification (Original_Body), No_List);
       Set_Defining_Unit_Name
         (Specification (Original_Body),
-          Make_Defining_Identifier (Sloc (N), Name_uParent));
+         Make_Defining_Identifier (Sloc (N), Name_uParent));
       Set_Corresponding_Spec (Original_Body, Empty);
 
-      --  Remove those pragmas that have no meaining in an inlined body.
+      --  Remove all aspects/pragmas that have no meaining in an inlined body
 
-      Remove_Pragmas (Original_Body);
+      Remove_Aspects_And_Pragmas (Original_Body);
 
       Body_To_Analyze := Copy_Generic_Node (Original_Body, Empty, False);
 
@@ -1116,8 +1127,9 @@ package body Inline is
       --  to be resolved.
 
       if Ekind (Spec_Id) = E_Function then
-         Set_Result_Definition (Specification (Body_To_Analyze),
-           New_Occurrence_Of (Etype (Spec_Id), Sloc (N)));
+         Set_Result_Definition
+           (Specification (Body_To_Analyze),
+            New_Occurrence_Of (Etype (Spec_Id), Sloc (N)));
       end if;
 
       if No (Declarations (N)) then
@@ -1126,9 +1138,9 @@ package body Inline is
          Append (Body_To_Analyze, Declarations (N));
       end if;
 
-      --  The body to inline is pre-analyzed.  In GNATprove mode we must
-      --  disable full analysis as well so that light expansion does not
-      --  take place either, and name resolution is unaffected.
+      --  The body to inline is pre-analyzed. In GNATprove mode we must disable
+      --  full analysis as well so that light expansion does not take place
+      --  either, and name resolution is unaffected.
 
       Expander_Mode_Save_And_Set (False);
       Full_Analysis := False;
@@ -1643,12 +1655,10 @@ package body Inline is
             Body_To_Inline := Copy_Separate_Tree (N);
          end if;
 
-         --  A pragma Unreferenced or pragma Unmodified that mentions a formal
-         --  parameter has no meaning when the body is inlined and the formals
-         --  are rewritten. Remove it from body to inline. The analysis of the
-         --  non-inlined body will handle the pragma properly.
+         --  Remove all aspects/pragmas that have no meaining in an inlined
+         --  body.
 
-         Remove_Pragmas (Body_To_Inline);
+         Remove_Aspects_And_Pragmas (Body_To_Inline);
 
          --  We need to capture references to the formals in order
          --  to substitute the actuals at the point of inlining, i.e.
@@ -3947,31 +3957,63 @@ package body Inline is
       end loop;
    end Remove_Dead_Instance;
 
-   --------------------
-   -- Remove_Pragmas --
-   --------------------
+   --------------------------------
+   -- Remove_Aspects_And_Pragmas --
+   --------------------------------
 
-   procedure Remove_Pragmas (Bod : Node_Id) is
-      Decl : Node_Id;
-      Nxt  : Node_Id;
+   procedure Remove_Aspects_And_Pragmas (Body_Decl : Node_Id) is
+      procedure Remove_Items (List : List_Id);
+      --  Remove all useless aspects/pragmas from a particular list
 
-   begin
-      Decl := First (Declarations (Bod));
-      while Present (Decl) loop
-         Nxt := Next (Decl);
+      ------------------
+      -- Remove_Items --
+      ------------------
 
-         if Nkind (Decl) = N_Pragma
-           and then Nam_In (Pragma_Name (Decl), Name_Contract_Cases,
-                                                Name_Precondition,
+      procedure Remove_Items (List : List_Id) is
+         Item      : Node_Id;
+         Item_Id   : Node_Id;
+         Next_Item : Node_Id;
+
+      begin
+         --  Traverse the list looking for an aspect specification or a pragma
+
+         Item := First (List);
+         while Present (Item) loop
+            Next_Item := Next (Item);
+
+            if Nkind (Item) = N_Aspect_Specification then
+               Item_Id := Identifier (Item);
+            elsif Nkind (Item) = N_Pragma then
+               Item_Id := Pragma_Identifier (Item);
+            else
+               Item_Id := Empty;
+            end if;
+
+            if Present (Item_Id)
+              and then Nam_In (Chars (Item_Id), Name_Contract_Cases,
+                                                Name_Global,
+                                                Name_Depends,
                                                 Name_Postcondition,
-                                                Name_Unreferenced,
-                                                Name_Unmodified)
-         then
-            Remove (Decl);
-         end if;
+                                                Name_Precondition,
+                                                Name_Refined_Global,
+                                                Name_Refined_Depends,
+                                                Name_Refined_Post,
+                                                Name_Test_Case,
+                                                Name_Unmodified,
+                                                Name_Unreferenced)
+            then
+               Remove (Item);
+            end if;
 
-         Decl := Nxt;
-      end loop;
-   end Remove_Pragmas;
+            Item := Next_Item;
+         end loop;
+      end Remove_Items;
+
+   --  Start of processing for Remove_Aspects_And_Pragmas
+
+   begin
+      Remove_Items (Aspect_Specifications (Body_Decl));
+      Remove_Items (Declarations          (Body_Decl));
+   end Remove_Aspects_And_Pragmas;
 
 end Inline;
diff --git a/gcc/ada/interfac.ads b/gcc/ada/interfac.ads
index 85ed9e956b7..6e3afffe5ee 100644
--- a/gcc/ada/interfac.ads
+++ b/gcc/ada/interfac.ads
@@ -51,12 +51,13 @@ package Interfaces is
    type Integer_32 is range -2 ** 31 .. 2 ** 31 - 1;
    for Integer_32'Size use 32;
 
-   type Integer_64 is range Long_Long_Integer'First .. Long_Long_Integer'Last;
+   type Integer_64 is new Long_Long_Integer;
    for Integer_64'Size use 64;
    --  Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this
-   --  unit to compile when using custom target configuration files where
-   --  the max integer is 32bits. This is useful for static analysis tools
-   --  such as SPARK or CodePeer.
+   --  unit to compile when using custom target configuration files where the
+   --  maximum integer is 32 bits. This is useful for static analysis tools
+   --  such as SPARK or CodePeer. In the normal case Long_Long_Integer is
+   --  always 64-bits so we get the desired 64-bit type.
 
    type Unsigned_8  is mod 2 ** 8;
    for Unsigned_8'Size use  8;
diff --git a/gcc/ada/namet.adb b/gcc/ada/namet.adb
index 1cebb464b8e..1a946402845 100644
--- a/gcc/ada/namet.adb
+++ b/gcc/ada/namet.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -1133,6 +1133,106 @@ package body Namet is
              T = V7;
    end Nam_In;
 
+   function Nam_In
+     (T  : Name_Id;
+      V1 : Name_Id;
+      V2 : Name_Id;
+      V3 : Name_Id;
+      V4 : Name_Id;
+      V5 : Name_Id;
+      V6 : Name_Id;
+      V7 : Name_Id;
+      V8 : Name_Id) return Boolean
+   is
+   begin
+      return T = V1 or else
+             T = V2 or else
+             T = V3 or else
+             T = V4 or else
+             T = V5 or else
+             T = V6 or else
+             T = V7 or else
+             T = V8;
+   end Nam_In;
+
+   function Nam_In
+     (T  : Name_Id;
+      V1 : Name_Id;
+      V2 : Name_Id;
+      V3 : Name_Id;
+      V4 : Name_Id;
+      V5 : Name_Id;
+      V6 : Name_Id;
+      V7 : Name_Id;
+      V8 : Name_Id;
+      V9 : Name_Id) return Boolean
+   is
+   begin
+      return T = V1 or else
+             T = V2 or else
+             T = V3 or else
+             T = V4 or else
+             T = V5 or else
+             T = V6 or else
+             T = V7 or else
+             T = V8 or else
+             T = V9;
+   end Nam_In;
+
+   function Nam_In
+     (T   : Name_Id;
+      V1  : Name_Id;
+      V2  : Name_Id;
+      V3  : Name_Id;
+      V4  : Name_Id;
+      V5  : Name_Id;
+      V6  : Name_Id;
+      V7  : Name_Id;
+      V8  : Name_Id;
+      V9  : Name_Id;
+      V10 : Name_Id) return Boolean
+   is
+   begin
+      return T = V1 or else
+             T = V2 or else
+             T = V3 or else
+             T = V4 or else
+             T = V5 or else
+             T = V6 or else
+             T = V7 or else
+             T = V8 or else
+             T = V9 or else
+             T = V10;
+   end Nam_In;
+
+   function Nam_In
+     (T   : Name_Id;
+      V1  : Name_Id;
+      V2  : Name_Id;
+      V3  : Name_Id;
+      V4  : Name_Id;
+      V5  : Name_Id;
+      V6  : Name_Id;
+      V7  : Name_Id;
+      V8  : Name_Id;
+      V9  : Name_Id;
+      V10 : Name_Id;
+      V11 : Name_Id) return Boolean
+   is
+   begin
+      return T = V1  or else
+             T = V2  or else
+             T = V3  or else
+             T = V4  or else
+             T = V5  or else
+             T = V6  or else
+             T = V7  or else
+             T = V8  or else
+             T = V9  or else
+             T = V10 or else
+             T = V11;
+   end Nam_In;
+
    ------------------
    -- Reinitialize --
    ------------------
diff --git a/gcc/ada/namet.ads b/gcc/ada/namet.ads
index 431204b6a77..a7d7a481636 100644
--- a/gcc/ada/namet.ads
+++ b/gcc/ada/namet.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -227,6 +227,56 @@ package Namet is
       V6 : Name_Id;
       V7 : Name_Id) return Boolean;
 
+   function Nam_In
+     (T  : Name_Id;
+      V1 : Name_Id;
+      V2 : Name_Id;
+      V3 : Name_Id;
+      V4 : Name_Id;
+      V5 : Name_Id;
+      V6 : Name_Id;
+      V7 : Name_Id;
+      V8 : Name_Id) return Boolean;
+
+   function Nam_In
+     (T  : Name_Id;
+      V1 : Name_Id;
+      V2 : Name_Id;
+      V3 : Name_Id;
+      V4 : Name_Id;
+      V5 : Name_Id;
+      V6 : Name_Id;
+      V7 : Name_Id;
+      V8 : Name_Id;
+      V9 : Name_Id) return Boolean;
+
+   function Nam_In
+     (T   : Name_Id;
+      V1  : Name_Id;
+      V2  : Name_Id;
+      V3  : Name_Id;
+      V4  : Name_Id;
+      V5  : Name_Id;
+      V6  : Name_Id;
+      V7  : Name_Id;
+      V8  : Name_Id;
+      V9  : Name_Id;
+      V10 : Name_Id) return Boolean;
+
+   function Nam_In
+     (T   : Name_Id;
+      V1  : Name_Id;
+      V2  : Name_Id;
+      V3  : Name_Id;
+      V4  : Name_Id;
+      V5  : Name_Id;
+      V6  : Name_Id;
+      V7  : Name_Id;
+      V8  : Name_Id;
+      V9  : Name_Id;
+      V10 : Name_Id;
+      V11 : Name_Id) return Boolean;
+
    pragma Inline (Nam_In);
    --  Inline all above functions
 
diff --git a/gcc/ada/s-crtl.ads b/gcc/ada/s-crtl.ads
index 959fa4a2eb3..217b5b6e593 100644
--- a/gcc/ada/s-crtl.ads
+++ b/gcc/ada/s-crtl.ads
@@ -62,11 +62,12 @@ package System.CRTL is
    type ssize_t is range -(2 ** (Standard'Address_Size - 1))
                       .. +(2 ** (Standard'Address_Size - 1)) - 1;
 
-   type int64 is range Long_Long_Integer'First .. Long_Long_Integer'Last;
+   type int64 is new Long_Long_Integer;
    --  Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this
-   --  unit to compile when using custom target configuration files where
-   --  the max integer is 32bits. This is useful for static analysis tools
-   --  such as SPARK or CodePeer.
+   --  unit to compile when using custom target configuration files where the
+   --  maximum integer is 32 bits. This is useful for static analysis tools
+   --  such as SPARK or CodePeer. In the normal case, Long_Long_Integer is
+   --  always 64-bits so there is no difference.
 
    type Filename_Encoding is (UTF8, ASCII_8bits, Unspecified);
    for Filename_Encoding use (UTF8 => 0, ASCII_8bits => 1, Unspecified => 2);
diff --git a/gcc/ada/s-taskin.ads b/gcc/ada/s-taskin.ads
index bf198ca3e80..ffb96c34640 100644
--- a/gcc/ada/s-taskin.ads
+++ b/gcc/ada/s-taskin.ads
@@ -947,7 +947,12 @@ package System.Tasking is
    --  by Ada.Task_Attributes.
 
    type Task_Serial_Number is mod 2 ** Long_Long_Integer'Size;
-   --  Used to give each task a unique serial number
+   --  Used to give each task a unique serial number. We want 64-bits for this
+   --  type to get as much uniqueness as possible (2**64 is operationally
+   --  infinite in this context, but 2**32 perhaps could recycle). We use
+   --  Long_Long_Integer (which in the normal case is always 64-bits) rather
+   --  than 64-bits explicitly to allow codepeer to analyze this unit when
+   --  a target configuration file forces the maximum integer size to 32.
 
    type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is record
       Common : Common_ATCB;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c26e4f2ebff..52853199a29 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -13920,11 +13920,12 @@ package body Sem_Prag is
          --  pragma Extensions_Visible [ (boolean_EXPRESSION) ];
 
          when Pragma_Extensions_Visible => Extensions_Visible : declare
-            Context : constant Node_Id := Parent (N);
-            Expr    : Node_Id;
-            Formal  : Entity_Id;
-            Subp    : Entity_Id;
-            Stmt    : Node_Id;
+            Context   : constant Node_Id := Parent (N);
+            Expr      : Node_Id;
+            Formal    : Entity_Id;
+            Orig_Stmt : Node_Id;
+            Subp      : Entity_Id;
+            Stmt      : Node_Id;
 
             Has_OK_Formal : Boolean := False;
 
@@ -13949,7 +13950,18 @@ package body Sem_Prag is
                --  Skip internally generated code
 
                elsif not Comes_From_Source (Stmt) then
-                  null;
+                  Orig_Stmt := Original_Node (Stmt);
+
+                  --  When pragma Ghost applies to an expression function, the
+                  --  expression function is transformed into a subprogram.
+
+                  if Nkind (Stmt) = N_Subprogram_Declaration
+                    and then Comes_From_Source (Orig_Stmt)
+                    and then Nkind (Orig_Stmt) = N_Expression_Function
+                  then
+                     Subp := Defining_Entity (Stmt);
+                     exit;
+                  end if;
 
                --  The associated [generic] subprogram declaration has been
                --  found, stop the search.
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 981d2193062..ba2135daa70 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -5923,7 +5923,8 @@ package body Sem_Util is
    function Extensions_Visible_Status
      (Id : Entity_Id) return Extensions_Visible_Mode
    is
-      Arg1 : Node_Id;
+      Arg  : Node_Id;
+      Decl : Node_Id;
       Expr : Node_Id;
       Prag : Node_Id;
       Subp : Entity_Id;
@@ -5946,15 +5947,51 @@ package body Sem_Util is
 
       Prag := Get_Pragma (Subp, Pragma_Extensions_Visible);
 
+      --  In certain cases analysis may request the Extensions_Visible status
+      --  of an expression function before the pragma has been analyzed yet.
+      --  Inspect the declarative items after the expression function looking
+      --  for the pragma (if any).
+
+      if No (Prag) and then Is_Expression_Function (Subp) then
+         Decl := Next (Unit_Declaration_Node (Subp));
+         while Present (Decl) loop
+            if Nkind (Decl) = N_Pragma
+              and then Pragma_Name (Decl) = Name_Extensions_Visible
+            then
+               Prag := Decl;
+               exit;
+
+            --  A source construct ends the region where Extensions_Visible may
+            --  appear, stop the traversal. An expanded expression function is
+            --  no longer a source construct, but it must still be recognized.
+
+            elsif Comes_From_Source (Decl)
+              or else (Nkind_In (Decl, N_Subprogram_Body,
+                                       N_Subprogram_Declaration)
+                         and then Is_Expression_Function
+                                    (Defining_Entity (Decl)))
+            then
+               exit;
+            end if;
+
+            Next (Decl);
+         end loop;
+      end if;
+
       --  Extract the value from the Boolean expression (if any)
 
       if Present (Prag) then
-         Arg1 := First (Pragma_Argument_Associations (Prag));
+         Arg := First (Pragma_Argument_Associations (Prag));
+
+         if Present (Arg) then
+            Expr := Get_Pragma_Arg (Arg);
 
-         --  The pragma appears with an argument
+            --  When the associated subprogram is an expression function, the
+            --  argument of the pragma may not have been analyzed.
 
-         if Present (Arg1) then
-            Expr := Get_Pragma_Arg (Arg1);
+            if not Analyzed (Expr) then
+               Preanalyze_And_Resolve (Expr, Standard_Boolean);
+            end if;
 
             --  Guard against cascading errors when the argument of pragma
             --  Extensions_Visible is not a valid static Boolean expression.
@@ -5969,19 +6006,20 @@ package body Sem_Util is
                return Extensions_Visible_False;
             end if;
 
-         --  Otherwise the pragma defaults to True
+         --  Otherwise the aspect or pragma defaults to True
 
          else
             return Extensions_Visible_True;
          end if;
 
-      --  Otherwise pragma Extensions_Visible is not inherited or directly
-      --  specified. In SPARK code, its value defaults to "False".
+      --  Otherwise aspect or pragma Extensions_Visible is not inherited or
+      --  directly specified. In SPARK code, its value defaults to "False".
 
       elsif SPARK_Mode = On then
          return Extensions_Visible_False;
 
-      --  In non-SPARK code, pragma Extensions_Visible defaults to "True"
+      --  In non-SPARK code, aspect or pragma Extensions_Visible defaults to
+      --  "True".
 
       else
          return Extensions_Visible_True;
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index f9c7052c4d3..ae7813593a1 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -562,7 +562,7 @@ package Sinfo is
    --  not make sense from a user point-of-view, and that cross-references that
    --  do not lead to data dependences for subprograms can be safely ignored.
 
-   --  GNATprove relies on the following frontend behaviors:
+   --  GNATprove relies on the following front end behaviors:
 
    --    1. The first declarations in the list of visible declarations of
    --       a package declaration for a generic instance, up to the first
@@ -579,13 +579,17 @@ package Sinfo is
 
    --    4. Unconstrained types are not replaced by constrained types whose
    --       bounds are generated from an expression: Expand_Subtype_From_Expr
-   --       should be noop.
+   --       should be a no-op.
 
-   --    5. Errors (instead of warnings) are issued on compile-time known
-   --       constraint errors, except in a few selected cases where it should
-   --       be allowed to let analysis proceed (e.g. range checks on empty
-   --       ranges, typically in deactivated code based on a given
-   --       configuration).
+   --    5. Errors (instead of warnings) are issued on compile-time-known
+   --       constraint errors even though such cases do not correspond to
+   --       illegalities in the Ada RM (this is simply another case where
+   --       GNATprove implements a subset of the full language).
+   --
+   --       However, there are a few exceptions to this rule for cases where
+   --       we want to allow the GNATprove analysis to proceed (e.g. range
+   --       checks on empty ranges, which typically appear in deactivated
+   --       code in a particular configuration).
 
    -----------------------
    -- Check Flag Fields --