diff mbox series

[Ada] Sync code for external properties with SPARK RM

Message ID 20201023082639.GA127458@adacore.com
State New
Headers show
Series [Ada] Sync code for external properties with SPARK RM | expand

Commit Message

Pierre-Marie de Rodat Oct. 23, 2020, 8:26 a.m. UTC 
Originally the allowed combinations of external properties (i.e.
Async_Readers, Async_Writers, Effective_Writes and Effective_Reads) were
described in the SPARK RM as a sequence of conditions. Then they have
been rewritten as a table and now the correspondence between description
in the SPARK RM and implementation in GNAT is not obvious.

This patch makes the implementation to mirror the description;
otherwise, semantics is unaffected.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_prag.adb (Check_External_Properties): Rewrite to match the
	SPARK RM description.
diff mbox series

Patch

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -29600,44 +29600,38 @@  package body Sem_Prag is
       ER   : Boolean;
       EW   : Boolean)
    is
-   begin
-      --  All properties enabled
-
-      if AR and AW and ER and EW then
-         null;
-
-      --  Async_Readers + Effective_Writes
-      --  Async_Readers + Async_Writers + Effective_Writes
-
-      elsif AR and EW and not ER then
-         null;
-
-      --  Async_Writers + Effective_Reads
-      --  Async_Readers + Async_Writers + Effective_Reads
-
-      elsif AW and ER and not EW then
-         null;
-
-      --  Async_Readers + Async_Writers
-
-      elsif AR and AW and not ER and not EW then
-         null;
+      type Properties is array (Positive range 1 .. 4) of Boolean;
+      type Combinations is array (Positive range <>) of Properties;
+      --  Arrays of Async_Readers, Async_Writers, Effective_Writes and
+      --  Effective_Reads properties and their combinations, respectively.
+
+      Specified : constant Properties := (AR, AW, EW, ER);
+      --  External properties, as given by the Item pragma
+
+      Allowed : constant Combinations :=
+        (1 => (True,  False, True,  False),
+         2 => (False, True,  False, True),
+         3 => (True,  False, False, False),
+         4 => (False, True,  False, False),
+         5 => (True,  True,  True,  False),
+         6 => (True,  True,  False, True),
+         7 => (True,  True,  False, False),
+         8 => (True,  True,  True,  True));
+      --  Allowed combinations, as listed in the SPARK RM 7.1.2(6) table
 
-      --  Async_Readers
-
-      elsif AR and not AW and not ER and not EW then
-         null;
-
-      --  Async_Writers
+   begin
+      --  Check if the specified properties match any of the allowed
+      --  combination; if not, then emit an error.
 
-      elsif AW and not AR and not ER and not EW then
-         null;
+      for J in Allowed'Range loop
+         if Specified = Allowed (J) then
+            return;
+         end if;
+      end loop;
 
-      else
-         SPARK_Msg_N
-           ("illegal combination of external properties (SPARK RM 7.1.2(6))",
-            Item);
-      end if;
+      SPARK_Msg_N
+        ("illegal combination of external properties (SPARK RM 7.1.2(6))",
+         Item);
    end Check_External_Properties;
 
    ----------------