aboutsummaryrefslogtreecommitdiff
path: root/gcc/testsuite/gnat.dg
diff options
context:
space:
mode:
authorClaire Dross <dross@adacore.com>2022-01-21 10:42:49 +0100
committerPierre-Marie de Rodat <derodat@adacore.com>2022-05-10 08:19:24 +0000
commitd89d9ecceb541ca824f7fb5f57f747a31c7ce9a5 (patch)
treee08429eef085f4446200987fdfbfc9708d79d12d /gcc/testsuite/gnat.dg
parent336ea8f2d6ef528db37212ac7517330274a4793a (diff)
downloadgcc-d89d9ecceb541ca824f7fb5f57f747a31c7ce9a5.zip
gcc-d89d9ecceb541ca824f7fb5f57f747a31c7ce9a5.tar.gz
gcc-d89d9ecceb541ca824f7fb5f57f747a31c7ce9a5.tar.bz2
[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.
Diffstat (limited to 'gcc/testsuite/gnat.dg')
-rw-r--r--gcc/testsuite/gnat.dg/loopvar.adb2
1 files changed, 1 insertions, 1 deletions
diff --git a/gcc/testsuite/gnat.dg/loopvar.adb b/gcc/testsuite/gnat.dg/loopvar.adb
index f85402a..e98d20d 100644
--- a/gcc/testsuite/gnat.dg/loopvar.adb
+++ b/gcc/testsuite/gnat.dg/loopvar.adb
@@ -9,7 +9,7 @@ begin
pragma Loop_Variant (J + 1); -- { dg-error "expect name \"Increases\"" }
pragma Loop_Variant (incr => -J + 1); -- { dg-error "expect name \"Increases\"" }
pragma Loop_Variant (decr => -J + 1); -- { dg-error "expect name \"Decreases\"" }
- pragma Loop_Variant (foof => -J + 1); -- { dg-error "expect name \"Increases\" or \"Decreases\"" }
+ pragma Loop_Variant (foof => -J + 1); -- { dg-error "expect name \"Increases\", \"Decreases\", or \"Structural\"" }
J := J + 2;
end loop;
end Loopvar;