]> gcc.gnu.org Git - gcc.git/commit
[Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant
authorClaire Dross <dross@adacore.com>
Fri, 21 Jan 2022 09:42:49 +0000 (10:42 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Tue, 10 May 2022 08:19:24 +0000 (08:19 +0000)
commitd89d9ecceb541ca824f7fb5f57f747a31c7ce9a5
treee08429eef085f4446200987fdfbfc9708d79d12d
parent336ea8f2d6ef528db37212ac7517330274a4793a
[Ada] Accept Structural in aspect Subprogram_Variant and pragma Loop_Variant

Add a new form of variants to ensure termination of loops or recursive
subprograms. Structural variants correspond to objects which designate a
part of the data-structure they used to designate in the previous loop
iteration or recursive call. They only imply termination if the
data-structure is acyclic, which is the case in SPARK but not in Ada in
general. The fact that these variants are correct is only verified
formally by the proof tool and not by the compiler or dynamically at
execution like other forms of variants.

gcc/ada/

* snames.ads-tmpl: Add "Structural" as a name.
* sem_prag.adb: (Analyze_Pragma): Accept modifier "Structural"
in pragmas Loop_Variant and Subprogram_Variant. Check that items
associated to Structural occur alone in the pragma associations.
(Analyze_Subprogram_Variant_In_Decl_Part): Idem.
* exp_prag.adb (Expand_Pragma_Loop_Variant): Discard structural
variants.
(Expand_Pragma_Subprogram_Variant): Idem.

gcc/testsuite/

* gnat.dg/loopvar.adb: Update expected error message.
gcc/ada/exp_prag.adb
gcc/ada/sem_prag.adb
gcc/ada/snames.ads-tmpl
gcc/testsuite/gnat.dg/loopvar.adb
This page took 0.069984 seconds and 6 git commands to generate.