[Ada] SPARK: fix bug related to non access object permissions
authorMaroua Maalej <maalej@adacore.com>
Tue, 9 Oct 2018 15:06:30 +0000 (15:06 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 9 Oct 2018 15:06:30 +0000 (15:06 +0000)
2018-10-09  Maroua Maalej  <maalej@adacore.com>

gcc/ada/

* sem_spark.adb (Check_Declaration): fix bug related to non
access object permissions.

From-SVN: r264979

gcc/ada/ChangeLog
gcc/ada/sem_spark.adb

index fdc2c3144129d5d990a96394819db3495bcdc341..fada99d05e1c019dbb46305f74fe10d37bd599f5 100644 (file)
@@ -1,3 +1,8 @@
+2018-10-09  Maroua Maalej  <maalej@adacore.com>
+
+       * sem_spark.adb (Check_Declaration): fix bug related to non
+       access object permissions.
+
 2018-10-09  Doug Rupp  <rupp@adacore.com>
 
        * libgnat/a-ncelfu.ads: Fix name in header to match package.
index 9a2209233b14c29040ed4b785146f9b74bc8b6fe..0fe7c1b881cd30ed7b90e68dd505f3c96f19dd48 100644 (file)
@@ -1052,22 +1052,6 @@ package body Sem_SPARK is
                      end if;
                   end if;
 
-               elsif Nkind_In (Expression (Decl),
-                               N_Attribute_Reference,
-                               N_Attribute_Reference,
-                               N_Expanded_Name,
-                               N_Explicit_Dereference,
-                               N_Indexed_Component,
-                               N_Reference,
-                               N_Selected_Component,
-                               N_Slice)
-               then
-                  if Is_Access_Type (Etype (Prefix (Expression (Decl))))
-                    or else Is_Deep (Etype (Prefix (Expression (Decl))))
-                  then
-                     Current_Checking_Mode := Observe;
-                     Check := True;
-                  end if;
                end if;
             end if;
 
@@ -1075,7 +1059,7 @@ package body Sem_SPARK is
                Check_Node (Expression (Decl));
             end if;
 
-            --  If lhs is not a pointer, we still give it the appropriate
+            --  If lhs is not a pointer, we still give it the unrestricted
             --  state which is useless but not harmful.
 
             declare
@@ -1215,7 +1199,7 @@ package body Sem_SPARK is
          when N_Attribute_Reference =>
             case Attribute_Name (Expr) is
                when Name_Access =>
-                  Error_Msg_N ("access attribute not allowed in SPARK", Expr);
+                  Error_Msg_N ("access attribute not allowed", Expr);
 
                when Name_Last
                   | Name_First