gcc/testsuite/gnat.dg/predicate14.ads

   1 generic
   2 package Predicate14 with
   3   SPARK_Mode
   4 is
   5
   6    type Field_Type is (F_Initial, F_Payload, F_Final);
   7
   8    type State_Type is (S_Valid, S_Invalid);
   9
  10    type Cursor_Type (State : State_Type := S_Invalid) is private;
  11
  12    type Cursors_Type is array (Field_Type) of Cursor_Type;
  13
  14    type Context_Type is private;
  15
  16    type Result_Type (Field : Field_Type := F_Initial) is
  17       record
  18          case Field is
  19             when F_Initial | F_Final =>
  20                null;
  21             when F_Payload =>
  22                Value : Integer;
  23          end case;
  24       end record;
  25
  26    function Valid_Context (Context : Context_Type) return Boolean;
  27
  28 private
  29
  30    function Valid_Type (Result : Result_Type) return Boolean is
  31      (Result.Field = F_Initial);
  32
  33    type Cursor_Type (State : State_Type := S_Invalid) is
  34       record
  35          case State is
  36             when S_Valid =>
  37                Value : Result_Type;
  38             when S_Invalid =>
  39                null;
  40          end case;
  41       end record
  42       with Dynamic_Predicate =>
  43           (if State = S_Valid then Valid_Type (Value));
  44
  45    type Context_Type is
  46       record
  47          Field : Field_Type := F_Initial;
  48          Cursors : Cursors_Type := (others => (State => S_Invalid));
  49       end record;
  50
  51    function Valid_Context (Context : Context_Type) return Boolean is
  52      (for all F in Context.Cursors'Range =>
  53          (Context.Cursors (F).Value.Field = F));
  54
  55    procedure Dummy;
  56 end Predicate14;