[Ada] Proof of System.Vectors.Boolean_Operations
commite5be83512a66369ae77c9652d3a3073a14ff466a
authorYannick Moy <moy@adacore.com>
Thu, 16 Dec 2021 15:42:36 +0000 (16 16:42 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Tue, 11 Jan 2022 13:24:46 +0000 (11 13:24 +0000)
treeec60839541fd858f961dab3436fec0adb2e5fb74
parentfb8e35819dada2d120817c9dae95703c0bb5841b
[Ada] Proof of System.Vectors.Boolean_Operations

gcc/ada/

* libgnat/s-veboop.adb: Add ghost code for proof.
* libgnat/s-veboop.ads: Add specification.
gcc/ada/libgnat/s-veboop.adb
gcc/ada/libgnat/s-veboop.ads