projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3795dac) | patch
[Ada] Annotate Ada.Synchronous_Barriers with SPARK_Mode => Off
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 25 Feb 2020 12:58:04 +0000 (13:58 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Tue, 9 Jun 2020 08:09:00 +0000 (04:09 -0400)
commit6859ef489341d436ebf2fd5d41282c4f68b0283d
tree9e9e8df800575371cb6aac225f0c06e947d87417tree
parent3795dac6fa7e6514cdc4daa138e29d5a4f4d001ecommit | diff
[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.
gcc/ada/libgnarl/a-synbar.adb diff | blob | history
gcc/ada/libgnarl/a-synbar.ads diff | blob | history
gcc/ada/libgnarl/a-synbar__posix.adb diff | blob | history
gcc/ada/libgnarl/a-synbar__posix.ads diff | blob | history