[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.
This commit is contained in:
parent
3795dac6fa
commit
6859ef4893
|
@ -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
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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 --
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in New Issue