[multiple changes]

2015-10-23  Gary Dismukes  <dismukes@adacore.com>

	* bindgen.adb, restrict.adb: Minor spelling/grammar fixes.

2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible
	elaboration issues in SPARK when the name denotes a source variable.

From-SVN: r229228

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 03a8dd91a156d9acb7b7e8ee9f54995424e3b180..5235631e0693440bf96769d1eebae4374b78179b 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,12 @@
+2015-10-23  Gary Dismukes  <dismukes@adacore.com>
+
+       * bindgen.adb, restrict.adb: Minor spelling/grammar fixes.
+
+2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * sem_res.adb (Resolve_Entity_Name): Code cleanup. Check for possible
+       elaboration issues in SPARK when the name denotes a source variable.
+
 2015-10-23  Hristian Kirtchev  <kirtchev@adacore.com>
 
        * exp_ch7.adb (Process_Transient_Objects): Reimplement to properly

diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb
index eb853b506f20df57daedaf89059e04433580094b..cf4b59f981a1e8e72cc3f863fc16031fe00b2917 100644 (file)
--- a/gcc/ada/bindgen.adb
+++ b/gcc/ada/bindgen.adb
@@ -2810,8 +2810,8 @@ package body Bindgen is
 
       procedure Check_Package (Var : in out Boolean; Name : String);
       --  Set Var to true iff the current identifier in Namet is Name. Do
-      --  nothing if it doesn't match. This procedure is just an helper to
-      --  avoid to explicitely deal with length.
+      --  nothing if it doesn't match. This procedure is just a helper to
+      --  avoid explicitly dealing with length.
 
       -------------------
       -- Check_Package --

diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 37f579b737a0a406ac1cdf1f7a0d4a71fa3ca908..b63b426d0967aea8253b129b70c2d099ded1f6cf 100644 (file)
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -503,7 +503,7 @@ package body Restrict is
       --  so that we have consistency between each compilation.
 
       --  In GNATprove mode restrictions are checked, except for
-      --  No_Initialize_Scalars, which is implicitely set in gnat1drv.adb.
+      --  No_Initialize_Scalars, which is implicitly set in gnat1drv.adb.
 
       --  Just checking, SPARK does not allow restrictions to be set ???
 

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 0a0c2897665a04afcb6316e1d33cd0e0f13d38be..62f82ebac92802b356c60dacf9e20ba0ea5f8829 100644 (file)
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7179,44 +7179,40 @@ package body Sem_Res is
          Par := Parent (Par);
       end if;
 
-      --  The following checks are only relevant when SPARK_Mode is on as they
-      --  are not standard Ada legality rules. An effectively volatile object
-      --  subject to enabled properties Async_Writers or Effective_Reads must
-      --  appear in a specific context.
-
-      if SPARK_Mode = On
-        and then Is_Object (E)
-        and then Is_Effectively_Volatile (E)
-        and then (Async_Writers_Enabled (E)
-                   or else Effective_Reads_Enabled (E))
-        and then Comes_From_Source (N)
-      then
-         --  The effectively volatile objects appears in a "non-interfering
-         --  context" as defined in SPARK RM 7.1.3(12).
+      if Comes_From_Source (N) then
 
-         if Is_OK_Volatile_Context (Par, N) then
-            null;
+         --  The following checks are only relevant when SPARK_Mode is on as
+         --  they are not standard Ada legality rules.
 
-         --  Otherwise the context causes a side effect with respect to the
-         --  effectively volatile object.
+         if SPARK_Mode = On then
 
-         else
-            SPARK_Msg_N
-              ("volatile object cannot appear in this context "
-               & "(SPARK RM 7.1.3(12))", N);
-         end if;
-      end if;
+            --  An effectively volatile object subject to enabled properties
+            --  Async_Writers or Effective_Reads must appear in non-interfering
+            --  context (SPARK RM 7.1.3(12)).
 
-      --  A Ghost entity must appear in a specific context
+            if Is_Object (E)
+              and then Is_Effectively_Volatile (E)
+              and then (Async_Writers_Enabled (E)
+                         or else Effective_Reads_Enabled (E))
+              and then not Is_OK_Volatile_Context (Par, N)
+            then
+               SPARK_Msg_N
+                 ("volatile object cannot appear in this context "
+                  & "(SPARK RM 7.1.3(12))", N);
+            end if;
 
-      if Is_Ghost_Entity (E) and then Comes_From_Source (N) then
-         Check_Ghost_Context (E, N);
-      end if;
+            --  Check possible elaboration issues with respect to variables
+
+            if Ekind (E) = E_Variable then
+               Check_Elab_Call (N);
+            end if;
+         end if;
 
-      --  In SPARK mode, need to check possible elaboration issues
+         --  A Ghost entity must appear in a specific context
 
-      if SPARK_Mode = On and then Ekind (E) = E_Variable then
-         Check_Elab_Call (N);
+         if Is_Ghost_Entity (E) then
+            Check_Ghost_Context (E, N);
+         end if;
       end if;
    end Resolve_Entity_Name;