diff mbox

[Ada] Further work on predicates

Message ID 20101022101017.GA4720@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 22, 2010, 10:10 a.m. UTC 
This patch completes the implementation of predicates as described in
AI05-0153-1/06. There are two more aspects to be taken care of. First
we will likely decide that 'First/'Last should not be allowed if a
predicate is present, second we want to introduce the notion of a
static predicate usable in case statements.

The following two tests are compiled with -gnata12 -gnatj60 -gnatld7
and they both execute silently showing that all tests have passed.

Compiling: test_predicates.ads

     1. with Ada.Assertions; use Ada.Assertions;
     2. package Test_Predicates is
     3.
     4.    type Even is range 0 .. Integer'Last with
     5.      Predicate => (Even mod 2) = 0;
     6.
     7.    type Color is
     8.      (Red, Orange, Yellow, Green, Blue, Indigo, Violet);
     9.    subtype RGB is Color with
    10.      Predicate => RGB = Red or RGB in Green .. Blue;
    11.    subtype Other_Color is Color with
    12.      Predicate => Other_Color not in RGB;
    13.
    14.    subtype Another_Color is Other_Color;
                   |
        >>> info: "Another_Color" inherits predicate from
            "Other_Color" at line 11

    15.    function Not_Another_One return Color;
    16.    -- Returns a value that violates
    17.    -- Another_Color's predicate
    18.
    19.    type No_Defaults is private;
    20.    subtype No_Defaults_P is No_Defaults with
    21.      Predicate => Is_Good (No_Defaults_P);
    22.
    23.    function Is_Good (X : No_Defaults) return Boolean;
    24.    function Good return No_Defaults;
    25.    function Bad return No_Defaults;
    26.    -- Is_Good(Good) is True; Is_Good(Bad) is False.
    27.
    28.    type Defaults is private;
    29.    subtype Defaults_P is Defaults with
    30.      Predicate => Is_Good (Defaults_P);
    31.
    32.    function Is_Good (X : Defaults) return Boolean;
    33.    function Good return Defaults;
    34.    function Bad return Defaults;
    35.
    36.    type String_Ref is access all String;
    37.
    38. private
    39.
    40.    type No_Defaults is
    41.       record
    42.          Comp : Integer;
    43.          Acc : String_Ref;
    44.          -- Default 'null' default doesn't count!
    45.       end record;
    46.
    47.    type Defaults is
    48.       record
    49.          Comp : Integer := 0;
    50.          Acc : String_Ref := null;
    51.       end record;
    52.
    53. end Test_Predicates;

Compiling: test_predicates.adb

     1.
     2. package body Test_Predicates is
     3.
     4.    function Not_Another_One return Color is
     5.    begin
     6.       return Result : constant Color := Red do
     7.          pragma Assert (Result in RGB);
     8.          pragma Assert
     9.            (Result not in Another_Color);
    10.       end return;
    11.    end Not_Another_One;
    12.
    13.    function Is_Good
    14.      (X : No_Defaults) return Boolean is
    15.    begin
    16.       return X.Acc /= null;
    17.    end Is_Good;
    18.
    19.    function Good return No_Defaults is
    20.    begin
    21.       return Result : constant No_Defaults
    22.         := (Comp => 0, Acc => new String'("xxx"))
    23.       do
    24.          pragma Assert (Result in No_Defaults_P);
    25.          pragma Assert (Is_Good (Result));
    26.       end return;
    27.    end Good;
    28.
    29.    function Bad return No_Defaults is
    30.    begin
    31.       return Result : constant No_Defaults
    32.         := (Comp => 0, Acc => null)
    33.       do
    34.          pragma Assert (Result not in No_Defaults_P);
    35.          pragma Assert (not Is_Good (Result));
    36.       end return;
    37.    end Bad;
    38.
    39.    function Is_Good (X : Defaults) return Boolean is
    40.    begin
    41.       return X.Acc /= null;
    42.    end Is_Good;
    43.
    44.    function Good return Defaults is
    45.    begin
    46.       return Result : constant Defaults
    47.         := (Comp => 0, Acc => new String'("xxx"))
    48.       do
    49.          pragma Assert (Is_Good (Result));
    50.          pragma Assert (Result in Defaults_P);
    51.       end return;
    52.    end Good;
    53.
    54.    function Bad return Defaults is
    55.    begin
    56.       return Result : constant Defaults
    57.         := (Comp => 0, Acc => null)
    58.       do
    59.          pragma Assert (not Is_Good (Result));
    60.          pragma Assert (Result not in Defaults_P);
    61.       end return;
    62.    end Bad;
    63.
    64. end Test_Predicates;

Compiling: test_predicates-acc.ads

     1. package Test_Predicates.Acc is
     2.
     3.    type Node (Discrim : Color) is
     4.       record
     5.          case Discrim is
     6.             when Red =>
     7.                Red_Comp : Integer;
     8.             when others =>
     9.                Others_Color_Comp : Integer;
    10.          end case;
    11.       end record;
    12.
    13.    type Ref is access all Node;
    14.    subtype RGB_Ref is Ref with
    15.      Predicate => RGB_Ref.all.Discrim in RGB;
    16.    subtype Another_Color_Ref is Ref with
    17.      Predicate =>
    18.        Another_Color_Ref.all.Discrim
    19.          in Another_Color;
    20.
    21. end Test_Predicates.Acc;

Compiling: test_predicates-main.adb

     1. with Test_Predicates.Acc;
     2. use Test_Predicates.Acc;
     3. procedure Test_Predicates.Main is
     4.    --  This test should run silently
     5.
     6.    pragma Assert (RGB'First in RGB);
     7.    pragma Assert
     8.      (Another_Color'First not in Another_Color);
     9.
    10.    pragma Assert (RGB'Last not in RGB);
    11.    pragma Assert
    12.      (Another_Color'Last in Another_Color);
    13.
    14.    X1 : RGB;
    15.    -- OK; predicate not checked
    16.
    17.    X2 : Another_Color;
    18.    -- OK; predicate not checked
    19.
    20.    X3 : No_Defaults;
    21.    -- OK; no predicate
    22.
    23.    X4 : No_Defaults_P;
    24.    -- OK; predicate not checked
    25.
    26.    X5 : Defaults;
    27.    -- OK; no predicate
    28.
    29.    X6 : RGB := Not_Another_One;
    30.    -- OK; predicate is True
    31.
    32.    X7 : No_Defaults := Bad;
    33.    -- OK; no predicate
    34.
    35.    X8 : No_Defaults_P := Good;
    36.    -- OK; predicate is True
    37.
    38.    X9 : Defaults := Bad;
    39.    -- OK; no predicate
    40.
    41.    X10 : Defaults_P := Good;
    42.    -- OK; predicate is True
    43.
    44.    Even_Var_1 : Even;
    45.    -- OK; predicate not checked
    46.
    47.    Even_Var_2 : Even := 100;
    48.    -- OK; predicate is True
    49.
    50. begin
    51.
    52.    begin
    53.       Even_Var_1 := 1;
    54.       raise Program_Error;
    55.       -- Predicate should have failed
    56.    exception
    57.       when Assertion_Error =>
    58.          null; -- OK
    59.    end;
    60.
    61.    Even_Var_1 := 0; -- OK; predicate is True
    62.
    63.    begin
    64.       declare
    65.          Even_Var_3 : Even := Even_Var_2 + 1;
    66.       begin
    67.          raise Program_Error;
    68.          -- Predicate should have failed
    69.       end;
    70.    exception
    71.       when Assertion_Error =>
    72.          null; -- OK
    73.    end;
    74.
    75.    ----------------
    76.
    77.    begin
    78.       declare
    79.          Var : Another_Color := Not_Another_One;
    80.       begin
    81.          raise Program_Error;
    82.          -- Predicate should have failed
    83.       end;
    84.    exception
    85.       when Assertion_Error =>
    86.          null; -- OK
    87.    end;
    88.
    89.    begin
    90.       declare
    91.          Var : Defaults_P := Bad;
    92.       begin
    93.          raise Program_Error;
    94.          -- Predicate should have failed
    95.       end;
    96.    exception
    97.       when Assertion_Error =>
    98.          null; -- OK
    99.    end;
   100.
   101.    begin
   102.       declare
   103.          Var : No_Defaults_P := Bad;
   104.       begin
   105.          raise Program_Error;
   106.          -- Predicate should have failed
   107.       end;
   108.    exception
   109.       when Assertion_Error =>
   110.          null; -- OK
   111.    end;
   112.
   113.    begin
   114.       declare
   115.          Var : Defaults_P;
   116.          -- Default init violates predicate
   117.       begin
   118.          raise Program_Error;
   119.          -- Predicate should have failed
   120.       end;
   121.    exception
   122.       when Assertion_Error =>
   123.          null; -- OK
   124.    end;
   125.
   126.    X1 := Not_Another_One; -- OK; predicate is True
   127.
   128.    begin
   129.       X2 := Not_Another_One;
   130.       raise Program_Error; -- Predicate should have failed
   131.    exception
   132.       when Assertion_Error =>
   133.          null; -- OK
   134.    end;
   135.
   136.    X3 := Bad; -- OK; no predicate
   137.
   138.    X4 := Good;
   139.    begin
   140.       X4 := Bad;
   141.       raise Program_Error;
   142.       -- Predicate should have failed
   143.    exception
   144.       when Assertion_Error =>
   145.          null; -- OK
   146.    end;
   147.
   148.    X5 := Bad; -- OK; no predicate
   149.
   150.    X6 := Not_Another_One;
   151.    -- OK; predicate is True
   152.
   153.    X7 := Bad; -- OK; no predicate
   154.
   155.    X8 := Good; -- OK; predicate is True
   156.    begin
   157.       X8 := Bad;
   158.       raise Program_Error;
   159.       -- Predicate should have failed
   160.    exception
   161.       when Assertion_Error =>
   162.          null; -- OK
   163.    end;
   164.
   165.    X9 := Bad; -- OK; no predicate
   166.
   167.    X10 := Good; -- OK; predicate is True
   168.    begin
   169.       X10 := Bad;
   170.       raise Program_Error;
   171.       -- Predicate should have failed
   172.    exception
   173.       when Assertion_Error =>
   174.          null; -- OK
   175.    end;
   176.
   177.    ----------------
   178.
   179.    declare
   180.       procedure P (X : Another_Color_Ref) is
   181.       begin
   182.          null;
   183.       end P;
   184.
   185.       Var : Ref := new Node(Red);
   186.    begin
   187.       P (Var); -- Violate predicate of 'in' param
   188.       raise Program_Error;
   189.    exception
   190.       when Assertion_Error =>
   191.          null; -- OK
   192.    end;
   193.
   194.    declare
   195.       procedure P (X : out Another_Color_Ref) is
   196.       begin
   197.          null;
   198.          -- Predicate of 'out' param
   199.          -- raises Constraint_Error
   200.       end P;
   201.
   202.       Var : Ref;
   203.    begin
   204.       P (Var);
   205.       raise Program_Error;
   206.    exception
   207.       when Constraint_Error =>
   208.          null; -- OK
   209.    end;
   210.
   211.    declare
   212.       procedure P (X : out Another_Color_Ref) is
   213.       begin
   214.          X := new Node(Orange);
   215.       end P;
   216.
   217.       Var : Ref;
   218.    begin
   219.       P (Var);
   220.       -- OK; don't check predicate on the way 'in'
   221.    end;
   222.
   223.    declare
   224.       procedure P (X : in out Another_Color_Ref) is
   225.       begin
   226.          X := new Node(Orange); -- Can't get here
   227.       end P;
   228.
   229.       Var : Ref;
   230.    begin
   231.       P (Var);
   232.       -- Predicate of 'in out' param
   233.       -- raises Constraint_Error
   234.       raise Program_Error;
   235.    exception
   236.       when Constraint_Error =>
   237.          null; -- OK
   238.    end;
   239.
   240. end Test_Predicates.Main;

Compiling: test_predicates_lim.ads

     1.
     2. with Ada.Assertions; use Ada.Assertions;
     3. package Test_Predicates_Lim is
     4.
     5.    type No_Defaults is limited private;
     6.    subtype No_Defaults_P is No_Defaults with
     7.      Predicate => Is_Good (No_Defaults_P);
     8.
     9.    function Is_Good (X : No_Defaults)
    10.      return Boolean;
    11.    function Good return No_Defaults;
    12.    function Bad return No_Defaults;
    13.    procedure Set_To_Bad (X : out No_Defaults);
    14.    procedure Set_To_Good (X : out No_Defaults);
    15.
    16.    type Defaults is limited private;
    17.    subtype Defaults_P is Defaults with
    18.      Predicate => Is_Good (Defaults_P);
    19.
    20.    function Is_Good (X : Defaults)
    21.      return Boolean;
    22.    function Good return Defaults;
    23.    function Bad return Defaults;
    24.    procedure Set_To_Bad (X : out Defaults);
    25.    procedure Set_To_Good (X : out Defaults);
    26.
    27.    type String_Ref is access all String;
    28.
    29. private
    30.
    31.    type No_Defaults is limited
    32.       record
    33.          Comp : Integer;
    34.          Acc : String_Ref;
    35.          -- Default 'null' default doesn't count!
    36.       end record;
    37.
    38.    type Defaults is limited
    39.       record
    40.          Comp : Integer := 0;
    41.          Acc : String_Ref := null;
    42.       end record;
    43.
    44. end Test_Predicates_Lim;

Compiling: test_predicates_lim.adb

     1. package body Test_Predicates_Lim is
     2.
     3.    function Is_Good (X : No_Defaults)
     4.      return Boolean is
     5.    begin
     6.       return X.Acc /= null;
     7.    end Is_Good;
     8.
     9.    function Good return No_Defaults is
    10.    begin
    11.       return Result : constant No_Defaults
    12.         := (Comp => 0, Acc => new String'("xxx"))
    13.       do
    14.          pragma Assert (Result in No_Defaults_P);
    15.          pragma Assert (Is_Good (Result));
    16.       end return;
    17.    end Good;
    18.
    19.    function Bad return No_Defaults is
    20.    begin
    21.       return Result : constant No_Defaults
    22.         := (Comp => 0, Acc => null)
    23.       do
    24.          pragma Assert
    25.            (Result not in No_Defaults_P);
    26.          pragma Assert (not Is_Good (Result));
    27.       end return;
    28.    end Bad;
    29.
    30.    procedure Set_To_Bad (X : out No_Defaults) is
    31.    begin
    32.       X.Acc := null;
    33.       pragma Assert (X not in No_Defaults_P);
    34.       pragma Assert (not Is_Good (X));
    35.    end Set_To_Bad;
    36.
    37.    procedure Set_To_Good (X : out No_Defaults) is
    38.    begin
    39.       X.Acc := new String'("xxx");
    40.       pragma Assert (X in No_Defaults_P);
    41.       pragma Assert (Is_Good (X));
    42.    end Set_To_Good;
    43.
    44.    function Is_Good (X : Defaults)
    45.      return Boolean is
    46.    begin
    47.       return X.Acc /= null;
    48.    end Is_Good;
    49.
    50.    function Good return Defaults is
    51.    begin
    52.       return Result : constant Defaults
    53.         := (Comp => 0,
    54.             Acc => new String'("xxx"))
    55.       do
    56.          pragma Assert (Is_Good (Result));
    57.          pragma Assert
    58.            (Result in Defaults_P);
    59.       end return;
    60.    end Good;
    61.
    62.    function Bad return Defaults is
    63.    begin
    64.       return Result : constant Defaults
    65.         := (Comp => 0, Acc => null)
    66.       do
    67.          pragma Assert
    68.            (not Is_Good (Result));
    69.          pragma Assert
    70.            (Result not in Defaults_P);
    71.       end return;
    72.    end Bad;
    73.
    74.    procedure Set_To_Bad (X : out Defaults) is
    75.    begin
    76.       X.Acc := null;
    77.       pragma Assert (X not in Defaults_P);
    78.       pragma Assert (not Is_Good (X));
    79.    end Set_To_Bad;
    80.
    81.    procedure Set_To_Good (X : out Defaults) is
    82.    begin
    83.       X.Acc := new String'("xxx");
    84.       pragma Assert (X in Defaults_P);
    85.       pragma Assert (Is_Good (X));
    86.    end Set_To_Good;
    87.
    88. end Test_Predicates_Lim;

Compiling: test_predicates_lim-main.adb

     1. pragma Warnings (Off);
     2. procedure Test_Predicates_Lim.Main is
     3.    --  This test should run silently
     4.
     5.    X3 : No_Defaults;
     6.    -- OK; no predicate
     7.
     8.    X4 : No_Defaults_P;
     9.    -- OK; predicate not checked
    10.
    11.    X5 : Defaults;
    12.    -- OK; no predicate
    13.
    14.    X7 : No_Defaults := Bad;
    15.    -- OK; no predicate
    16.
    17.    X8 : No_Defaults_P := Good;
    18.    -- OK; predicate is True
    19.
    20.    X9 : Defaults := Bad;
    21.    -- OK; no predicate
    22.
    23.    X10 : Defaults := Good;
    24.    -- OK; predicate is True
    25.
    26. begin
    27.
    28.    begin
    29.       declare
    30.          Var : Defaults_P;
    31.          -- Default init violates predicate
    32.       begin
    33.          raise Program_Error;
    34.          -- Predicate should have failed
    35.       end;
    36.    exception
    37.       when Assertion_Error =>
    38.          null; -- OK
    39.    end;
    40.
    41.    begin
    42.       declare
    43.          Var : Defaults_P := Bad;
    44.       begin
    45.          raise Program_Error;
    46.          -- Predicate should have failed
    47.       end;
    48.    exception
    49.       when Assertion_Error =>
    50.          null; -- OK
    51.    end;
    52.
    53.    begin
    54.       declare
    55.          Var : No_Defaults_P := Bad;
    56.       begin
    57.          raise Program_Error;
    58.          -- Predicate should have failed
    59.       end;
    60.    exception
    61.       when Assertion_Error =>
    62.          null; -- OK
    63.    end;
    64.
    65.    declare
    66.       procedure P (X : No_Defaults_P) is
    67.       begin
    68.          null;
    69.       end P;
    70.    begin
    71.       P (Bad);
    72.       -- Violate predicate of 'in' param
    73.    exception
    74.       when Assertion_Error =>
    75.          null; -- OK
    76.          P (Good);
    77.    end;
    78.
    79.    declare
    80.       procedure P (X : out No_Defaults_P) is
    81.       begin
    82.          Set_To_Bad (X);
    83.          -- Violate predicate of 'out' param
    84.       end P;
    85.       X : No_Defaults := Good;
    86.    begin
    87.       P (X);
    88.    exception
    89.       when Assertion_Error =>
    90.          null; -- OK
    91.    end;
    92.
    93.    declare
    94.       procedure P (X : out No_Defaults_P) is
    95.       begin
    96.          Set_To_Good (X);
    97.       end P;
    98.       X : No_Defaults := Bad;
    99.       -- OK; no predicate
   100.    begin
   101.       P (X);
   102.       -- OK; no check for 'out' on the way in
   103.    end;
   104.
   105.    declare
   106.       procedure P (X : in out No_Defaults_P) is
   107.       begin
   108.          Set_To_Bad (X);
   109.          -- Violate predicate of 'in out' param
   110.       end P;
   111.       X : No_Defaults := Good;
   112.    begin
   113.       P (X);
   114.    exception
   115.       when Assertion_Error =>
   116.          null; -- OK
   117.    end;
   118.
   119. end Test_Predicates_Lim.Main;

Tested on x86_64-pc-linux-gnu, committed on trunk

2010-10-22  Robert Dewar  <dewar@adacore.com>

	* exp_ch3.adb (Expand_N_Object_Declaration): Do required predicate
	checks.
	* sem_ch3.adb (Complete_Private_Subtype): Propagate predicates to full
	view.
	* sem_ch6.adb (Invariants_Or_Predicates_Present): New name for
	Invariants_Present.
	(Process_PPCs): Handle predicates generating post conditions
	* sem_util.adb (Is_Partially_Initialized_Type): Add
	Include_Null parameter.
	* sem_util.ads (Is_Partially_Initialized_Type): Add
	Include_Null parameter.
diff mbox

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 165805)
+++ sem_ch3.adb	(working copy)
@@ -9913,6 +9913,13 @@  package body Sem_Ch3 is
               Corresponding_Record_Type (Full_Base));
          end if;
       end if;
+
+      --  Copy rep item chain, and also setting of Has_Predicates from
+      --  private subtype to full subtype, since we will need these on the
+      --  full subtype to create the predicate function.
+
+      Set_First_Rep_Item (Full, First_Rep_Item (Priv));
+      Set_Has_Predicates (Full, Has_Predicates (Priv));
    end Complete_Private_Subtype;
 
    ----------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 165811)
+++ sem_util.adb	(working copy)
@@ -6776,19 +6776,24 @@  package body Sem_Util is
    -- Is_Partially_Initialized_Type --
    -----------------------------------
 
-   function Is_Partially_Initialized_Type (Typ : Entity_Id) return Boolean is
+   function Is_Partially_Initialized_Type
+     (Typ          : Entity_Id;
+      Include_Null : Boolean := True) return Boolean
+   is
    begin
       if Is_Scalar_Type (Typ) then
          return False;
 
       elsif Is_Access_Type (Typ) then
-         return True;
+         return Include_Null;
 
       elsif Is_Array_Type (Typ) then
 
          --  If component type is partially initialized, so is array type
 
-         if Is_Partially_Initialized_Type (Component_Type (Typ)) then
+         if Is_Partially_Initialized_Type
+              (Component_Type (Typ), Include_Null)
+         then
             return True;
 
          --  Otherwise we are only partially initialized if we are fully
@@ -6841,7 +6846,9 @@  package body Sem_Util is
                      --  If a component is of a type which is itself partially
                      --  initialized, then the enclosing record type is also.
 
-                     elsif Is_Partially_Initialized_Type (Etype (Ent)) then
+                     elsif Is_Partially_Initialized_Type
+                             (Etype (Ent), Include_Null)
+                     then
                         return True;
                      end if;
                   end if;
@@ -6880,7 +6887,7 @@  package body Sem_Util is
             if No (U) then
                return True;
             else
-               return Is_Partially_Initialized_Type (U);
+               return Is_Partially_Initialized_Type (U, Include_Null);
             end if;
          end;
 
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 165811)
+++ sem_util.ads	(working copy)
@@ -760,12 +760,18 @@  package Sem_Util is
    --  the Is_Variable sense) with a non-tagged type target are considered view
    --  conversions and hence variables.
 
-   function Is_Partially_Initialized_Type (Typ : Entity_Id) return Boolean;
+   function Is_Partially_Initialized_Type
+     (Typ          : Entity_Id;
+      Include_Null : Boolean := True) return Boolean;
    --  Typ is a type entity. This function returns true if this type is partly
    --  initialized, meaning that an object of the type is at least partly
    --  initialized (in particular in the record case, that at least one
    --  component has an initialization expression). Note that initialization
    --  resulting from the use of pragma Normalized_Scalars does not count.
+   --  Include_Null controls the handling of access types, and components of
+   --  access types not explicitly initialized. If set to True, the default,
+   --  default initialization of access types counts as making the type be
+   --  partially initialized. If False, this does not count.
 
    function Is_Potentially_Persistent_Type (T : Entity_Id) return Boolean;
    --  Determines if type T is a potentially persistent type. A potentially
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165812)
+++ sem_ch6.adb	(working copy)
@@ -207,8 +207,8 @@  package body Sem_Ch6 is
    --  conditions for the body and assembling and inserting the _postconditions
    --  procedure. N is the node for the subprogram body and Body_Id/Spec_Id are
    --  the entities for the body and separate spec (if there is no separate
-   --  spec, Spec_Id is Empty). Note that invariants also provide a source
-   --  of postconditions, which are also handled in this procedure.
+   --  spec, Spec_Id is Empty). Note that invariants and predicates may also
+   --  provide postconditions, and are also handled in this procedure.
 
    procedure Set_Formal_Validity (Formal_Id : Entity_Id);
    --  Formal_Id is an formal parameter entity. This procedure deals with
@@ -8681,9 +8681,10 @@  package body Sem_Ch6 is
       --  references to parameters of the inherited subprogram to point to the
       --  corresponding parameters of the current subprogram.
 
-      function Invariants_Present return Boolean;
-      --  Determines if any invariants are present for any OUT or IN OUT
-      --  parameters of the subprogram, or (for a function) for the return.
+      function Invariants_Or_Predicates_Present return Boolean;
+      --  Determines if any invariants or predicates are present for any OUT
+      --  or IN OUT parameters of the subprogram, or (for a function) if the
+      --  return value has an invariant.
 
       --------------
       -- Grab_PPC --
@@ -8782,12 +8783,12 @@  package body Sem_Ch6 is
          return CP;
       end Grab_PPC;
 
-      ------------------------
-      -- Invariants_Present --
-      ------------------------
+      --------------------------------------
+      -- Invariants_Or_Predicates_Present --
+      --------------------------------------
 
-      function Invariants_Present return Boolean is
-         Formal     : Entity_Id;
+      function Invariants_Or_Predicates_Present return Boolean is
+         Formal : Entity_Id;
 
       begin
          --  Check function return result
@@ -8803,7 +8804,9 @@  package body Sem_Ch6 is
          Formal := First_Formal (Designator);
          while Present (Formal) loop
             if Ekind (Formal) /= E_In_Parameter
-              and then Has_Invariants (Etype (Formal))
+              and then
+                (Has_Invariants (Etype (Formal))
+                  or else Present (Predicate_Function (Etype (Formal))))
             then
                return True;
             end if;
@@ -8812,7 +8815,7 @@  package body Sem_Ch6 is
          end loop;
 
          return False;
-      end Invariants_Present;
+      end Invariants_Or_Predicates_Present;
 
    --  Start of processing for Process_PPCs
 
@@ -9084,7 +9087,7 @@  package body Sem_Ch6 is
       --  If we had any postconditions and expansion is enabled, or if the
       --  procedure has invariants, then build the _Postconditions procedure.
 
-      if (Present (Plist) or else Invariants_Present)
+      if (Present (Plist) or else Invariants_Or_Predicates_Present)
         and then Expander_Active
       then
          if No (Plist) then
@@ -9127,21 +9130,33 @@  package body Sem_Ch6 is
             Parms := No_List;
          end if;
 
-         --  Add invariant calls for parameters. Note that this is done for
-         --  functions as well, since in Ada 2012 they can have IN OUT args.
+         --  Add invariant calls and predicate calls for parameters. Note that
+         --  this is done for functions as well, since in Ada 2012 they can
+         --  have IN OUT args.
 
          declare
             Formal : Entity_Id;
+            Ftype  : Entity_Id;
 
          begin
             Formal := First_Formal (Designator);
             while Present (Formal) loop
-               if Ekind (Formal) /= E_In_Parameter
-                 and then Has_Invariants (Etype (Formal))
-                 and then Present (Invariant_Procedure (Etype (Formal)))
-               then
-                  Append_To (Plist,
-                    Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)));
+               if Ekind (Formal) /= E_In_Parameter then
+                  Ftype := Etype (Formal);
+
+                  if Has_Invariants (Ftype)
+                    and then Present (Invariant_Procedure (Ftype))
+                  then
+                     Append_To (Plist,
+                       Make_Invariant_Call
+                         (New_Occurrence_Of (Formal, Loc)));
+                  end if;
+
+                  if Present (Predicate_Function (Ftype)) then
+                     Append_To (Plist,
+                       Make_Predicate_Check
+                         (Ftype, New_Occurrence_Of (Formal, Loc)));
+                  end if;
                end if;
 
                Next_Formal (Formal);
@@ -9365,6 +9380,7 @@  package body Sem_Ch6 is
          if Ekind (Scope (Formal_Id)) = E_Function
            or else Ekind (Scope (Formal_Id)) = E_Generic_Function
          then
+            --  [IN] OUT parameters allowed for functions in Ada 2012
 
             if Ada_Version >= Ada_2012 then
                if In_Present (Spec) then
@@ -9373,6 +9389,8 @@  package body Sem_Ch6 is
                   Set_Ekind (Formal_Id, E_Out_Parameter);
                end if;
 
+            --  But not in earlier versions of Ada
+
             else
                Error_Msg_N ("functions can only have IN parameters", Spec);
                Set_Ekind (Formal_Id, E_In_Parameter);
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 165803)
+++ exp_ch3.adb	(working copy)
@@ -4508,6 +4508,24 @@  package body Exp_Ch3 is
          return;
       end if;
 
+      --  Deal with predicate check before we start to do major rewriting.
+      --  it is OK to initialize and then check the initialized value, since
+      --  the object goes out of scope if we get a predicate failure.
+
+      --  We need a predicate check if the type has predicates, and if either
+      --  there is an initializing expression, or for default initialization
+      --  when we have at least one case of an explicit default initial value.
+
+      if Present (Predicate_Function (Typ))
+        and then
+          (Present (Expr)
+            or else
+              Is_Partially_Initialized_Type (Typ, Include_Null => False))
+      then
+         Insert_After (N,
+           Make_Predicate_Check (Typ, New_Occurrence_Of (Def_Id, Loc)));
+      end if;
+
       --  Force construction of dispatch tables of library level tagged types
 
       if Tagged_Type_Expansion