diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-02-25 13:58:04 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-09 04:09:00 -0400 |
| commit | 6859ef489341d436ebf2fd5d41282c4f68b0283d (patch) | |
| tree | 9e9e8df800575371cb6aac225f0c06e947d87417 | |
| parent | 3795dac6fa7e6514cdc4daa138e29d5a4f4d001e (diff) | |
| download | gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.zip gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.tar.gz gcc-6859ef489341d436ebf2fd5d41282c4f68b0283d.tar.bz2 | |
[Ada] Annotate Ada.Synchronous_Barriers with SPARK_Mode => Off
2020-06-09 Piotr Trojanek <trojanek@adacore.com>
gcc/ada/
* libgnarl/a-synbar.ads, libgnarl/a-synbar.adb,
libgnarl/a-synbar__posix.ads, libgnarl/a-synbar__posix.adb
(Ada.Synchronous_Barriers): Annotate with SPARK_Mode => Off.
| -rw-r--r-- | gcc/ada/libgnarl/a-synbar.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnarl/a-synbar.ads | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnarl/a-synbar__posix.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnarl/a-synbar__posix.ads | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/gcc/ada/libgnarl/a-synbar.adb b/gcc/ada/libgnarl/a-synbar.adb index 6f5664d..df4f9f4 100644 --- a/gcc/ada/libgnarl/a-synbar.adb +++ b/gcc/ada/libgnarl/a-synbar.adb @@ -33,7 +33,7 @@ -- -- ------------------------------------------------------------------------------ -package body Ada.Synchronous_Barriers is +package body Ada.Synchronous_Barriers with SPARK_Mode => Off is protected body Synchronous_Barrier is diff --git a/gcc/ada/libgnarl/a-synbar.ads b/gcc/ada/libgnarl/a-synbar.ads index 3458e58..c423695 100644 --- a/gcc/ada/libgnarl/a-synbar.ads +++ b/gcc/ada/libgnarl/a-synbar.ads @@ -33,7 +33,7 @@ -- -- ------------------------------------------------------------------------------ -package Ada.Synchronous_Barriers is +package Ada.Synchronous_Barriers with SPARK_Mode => Off is pragma Preelaborate (Synchronous_Barriers); subtype Barrier_Limit is Positive range 1 .. Positive'Last; diff --git a/gcc/ada/libgnarl/a-synbar__posix.adb b/gcc/ada/libgnarl/a-synbar__posix.adb index 295047c..96f4a7b 100644 --- a/gcc/ada/libgnarl/a-synbar__posix.adb +++ b/gcc/ada/libgnarl/a-synbar__posix.adb @@ -37,7 +37,7 @@ with Interfaces.C; use Interfaces.C; -package body Ada.Synchronous_Barriers is +package body Ada.Synchronous_Barriers with SPARK_Mode => Off is -------------------- -- POSIX barriers -- diff --git a/gcc/ada/libgnarl/a-synbar__posix.ads b/gcc/ada/libgnarl/a-synbar__posix.ads index 553725c..afbeb6b 100644 --- a/gcc/ada/libgnarl/a-synbar__posix.ads +++ b/gcc/ada/libgnarl/a-synbar__posix.ads @@ -39,7 +39,7 @@ with System; private with Ada.Finalization; private with Interfaces.C; -package Ada.Synchronous_Barriers is +package Ada.Synchronous_Barriers with SPARK_Mode => Off is pragma Preelaborate (Synchronous_Barriers); subtype Barrier_Limit is Positive range 1 .. Positive'Last; |