[multiple changes]

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_Protected_Operation_Call):
	Add guards to account for a non-decorated selected component.

2016-04-18  Yannick Moy  <moy@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve
	implementation of Body_Has_SPARK_Mode_On.
	* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation):
	New function replacing previous Get_SPARK_Mode_From_Pragma, that
	deals also with aspects.
	(Get_SPARK_Mode_Type): Make function internal again.
	* inline.adb, sem_ch7.adb, sem_util.adb: Use new
	Get_SPARK_Mode_From_Annotation.

From-SVN: r235116

8 files changed, 84 insertions, 42 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9691433..fd8d79a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,21 @@
 2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* sem_res.adb (Is_Protected_Operation_Call):
+	Add guards to account for a non-decorated selected component.
+
+2016-04-18  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve
+	implementation of Body_Has_SPARK_Mode_On.
+	* sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation):
+	New function replacing previous Get_SPARK_Mode_From_Pragma, that
+	deals also with aspects.
+	(Get_SPARK_Mode_Type): Make function internal again.
+	* inline.adb, sem_ch7.adb, sem_util.adb: Use new
+	Get_SPARK_Mode_From_Annotation.
+
+2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* contracts.adb (Analyze_Object_Contract): Update references to
 	SPARK RM.
 	* freeze.adb (Freeze_Entity): Update references to SPARK RM.
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 9a7b375..b3b5aba 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1553,7 +1553,8 @@ package body Inline is
       elsif Present (Spec_Id)
         and then
           (No (SPARK_Pragma (Spec_Id))
-            or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
+            or else
+           Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On)
       then
          return False;
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 17c2623..9563320 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2292,11 +2292,7 @@ package body Sem_Ch6 is
             Item := First (Aspect_Specifications (N));
             while Present (Item) loop
                if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then
-                  return No (Expression (Item))
-                           or else
-                        (Nkind (Expression (Item)) = N_Identifier
-                           and then
-                         Get_SPARK_Mode_Type (Chars (Expression (Item))) = On);
+                  return Get_SPARK_Mode_From_Annotation (Item) = On;
                end if;
 
                Next (Item);
@@ -2308,18 +2304,28 @@ package body Sem_Ch6 is
          if Present (Decls) then
             Item := First (Decls);
             while Present (Item) loop
-               if Nkind (Item) = N_Pragma
-                 and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode
-               then
-                  return Get_SPARK_Mode_From_Pragma (Item) = On;
+
+               --  Pragmas that apply to a subprogram body are usually grouped
+               --  together. Look for a potential pragma SPARK_Mode among them.
+
+               if Nkind (Item) = N_Pragma then
+                  if Get_Pragma_Id (Item) = Pragma_SPARK_Mode then
+                     return Get_SPARK_Mode_From_Annotation (Item) = On;
+                  end if;
+
+               --  Otherwise the first non-pragma declarative item terminates
+               --  the region where pragma SPARK_Mode may appear.
+
+               else
+                  exit;
                end if;
 
                Next (Item);
             end loop;
          end if;
 
-         --  Applicable SPARK_Mode is inherited from the enclosing subprogram
-         --  or package.
+         --  Otherwise, the applicable SPARK_Mode is inherited from the
+         --  enclosing subprogram or package.
 
          return SPARK_Mode = On;
       end Body_Has_SPARK_Mode_On;
@@ -3849,9 +3855,9 @@ package body Sem_Ch6 is
 
       if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Pragma (Spec_Id)) then
-            if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+            if Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) = Off
                  and then
-               Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+               Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
             then
                Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
                Error_Msg_N ("incorrect application of SPARK_Mode#", N);
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index e182771..b332f20 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -777,9 +777,10 @@ package body Sem_Ch7 is
 
       if Present (SPARK_Pragma (Body_Id)) then
          if Present (SPARK_Aux_Pragma (Spec_Id)) then
-            if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
-                 and then
-               Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+            if Get_SPARK_Mode_From_Annotation (SPARK_Aux_Pragma (Spec_Id)) =
+                 Off
+              and then
+                Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
             then
                Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
                Error_Msg_N ("incorrect application of SPARK_Mode#", N);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index e951804..7be7172 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -235,6 +235,11 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
+   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+   --  Get_SPARK_Mode_From_Annotation. Convert a name into a corresponding
+   --  value of type SPARK_Mode_Type.
+
    function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
    --  Subsidiary to the analysis of pragmas Depends and Refined_Depends.
    --  Determine whether dependency clause Clause is surrounded by extra
@@ -20338,8 +20343,8 @@ package body Sem_Prag is
                   --  Issue an error if the new mode is less restrictive than
                   --  that of the context.
 
-                  if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
-                    and then Get_SPARK_Mode_From_Pragma (N) = On
+                  if Get_SPARK_Mode_From_Annotation (Context_Pragma) = Off
+                    and then Get_SPARK_Mode_From_Annotation (N) = On
                   then
                      Error_Msg_N
                        ("cannot change SPARK_Mode from Off to On", Err_N);
@@ -20376,8 +20381,8 @@ package body Sem_Prag is
                      --  Issue an error if the new mode is less restrictive
                      --  than that of the initial declaration.
 
-                     if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
-                       and then Get_SPARK_Mode_From_Pragma (N) = On
+                     if Get_SPARK_Mode_From_Annotation (Entity_Pragma) = Off
+                       and then Get_SPARK_Mode_From_Annotation (N) = On
                      then
                         Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
                         Error_Msg_Sloc := Sloc (Entity_Pragma);
@@ -27553,30 +27558,45 @@ package body Sem_Prag is
       end if;
    end Get_SPARK_Mode_Type;
 
-   --------------------------------
-   -- Get_SPARK_Mode_From_Pragma --
-   --------------------------------
+   ------------------------------------
+   -- Get_SPARK_Mode_From_Annotation --
+   ------------------------------------
 
-   function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is
-      Args : List_Id;
+   function Get_SPARK_Mode_From_Annotation
+     (N : Node_Id) return SPARK_Mode_Type
+   is
       Mode : Node_Id;
 
    begin
-      pragma Assert (Nkind (N) = N_Pragma);
-      Args := Pragma_Argument_Associations (N);
+      if Nkind (N) = N_Aspect_Specification then
+         Mode := Expression (N);
 
-      --  Extract the mode from the argument list
-
-      if Present (Args) then
+      else pragma Assert (Nkind (N) = N_Pragma);
          Mode := First (Pragma_Argument_Associations (N));
-         return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode)));
 
-      --  If SPARK_Mode pragma has no argument, default is ON
+         if Present (Mode) then
+            Mode := Get_Pragma_Arg (Mode);
+         end if;
+      end if;
+
+      --  Aspect or pragma SPARK_Mode specifies an explicit mode
+
+      if Present (Mode) then
+         if Nkind (Mode) = N_Identifier then
+            return Get_SPARK_Mode_Type (Chars (Mode));
+
+         --  In case of a malformed aspect or pragma, return the default None
+
+         else
+            return None;
+         end if;
+
+      --  Otherwise the lack of an expression defaults SPARK_Mode to On
 
       else
          return On;
       end if;
-   end Get_SPARK_Mode_From_Pragma;
+   end Get_SPARK_Mode_From_Annotation;
 
    ---------------------------
    -- Has_Extra_Parentheses --
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 063e7df..a78478e 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -397,13 +397,9 @@ package Sem_Prag is
    --  Context denotes the entity of the function, package or procedure where
    --  Prag resides.
 
-   function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
-   --  Given a pragma SPARK_Mode node, return corresponding mode id
-
-   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
-   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
-   --  Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value
-   --  of type SPARK_Mode_Type.
+   function Get_SPARK_Mode_From_Annotation
+     (N : Node_Id) return SPARK_Mode_Type;
+   --  Given an aspect or pragma SPARK_Mode node, return corresponding mode id
 
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 18794c8..c12356c 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6895,8 +6895,10 @@ package body Sem_Res is
 
                return
                  Pref = Obj_Ref
+                   and then Present (Etype (Pref))
                    and then Is_Protected_Type (Etype (Pref))
                    and then Is_Entity_Name (Subp)
+                   and then Present (Entity (Subp))
                    and then Ekind_In (Entity (Subp), E_Entry,
                                                      E_Entry_Family,
                                                      E_Function,
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7bfe724..1146b9d 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -18645,7 +18645,7 @@ package body Sem_Util is
          null;
 
       elsif Present (SPARK_Pragma (Context)) then
-         SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Context));
+         SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context));
       end if;
    end Save_SPARK_Mode_And_Set;