gcc/testsuite/gnat.dg/expr_func8.adb

   1 --  { dg-do compile }
   2 --  { dg-options "-gnata" }
   3
   4 procedure Expr_Func8 is
   5
   6    type Node_Set is array (Positive range <>) of Integer;
   7
   8    function Nodes return Node_Set is
   9      ((1,2,3,4,5,6,7,8,9));
  10
  11    X1 : Boolean := (for all N of Nodes => N = N);
  12
  13    function Predecessors (N : Integer) return Node_Set Is
  14       (Nodes (1 .. N - 1));
  15    function Successors (N : Integer) return Node_Set Is
  16       (Nodes (N + 1 .. Nodes'Last));
  17
  18    pragma Assert
  19      (for all N of Nodes =>
  20        (for some S of Successors (N) => S = N));
  21
  22    X2 : Boolean :=
  23      (for all N of Nodes =>
  24        (for some S of Successors (N) => S = N));
  25
  26    X3 : Boolean :=
  27      (for all N of Nodes =>
  28        (for some S of Successors (N) => S = N)) with Ghost;
  29
  30    pragma Assert
  31       (for all N of Nodes =>
  32       (for all P of Predecessors (N) =>
  33       (for some S of Successors (P) => S = N)));
  34
  35 begin
  36    null;
  37 end;