[Ada] Suppress the expansion of ignored assertion pragmas

This patch suppresses the expansion of ignored assertion pragmas.

2018-06-11  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* contracts.adb (Process_Body_Postconditions): Expand only checked
	postconditions.
	(Process_Contract_Cases_For): Expand only checked contract cases.
	(Process_Inherited_Preconditions): Ignored class-wide preconditions are
	partially expanded because some of their semantic checks are tied to
	the expansion.
	(Process_Preconditions_For): Expand only checked preconditions.
	(Process_Spec_Postconditions): Expand only checked preconditions.
	Ignored class-wide preconditions are partially expanded because some of
	their semantic checks are tied to the expansion.
	* exp_prag.adb (Expand_N_Pragma): Suppress the expansion of ignored
	assertion pragmas.
	* exp_util.adb (Add_Inherited_Invariants): Code clean up.
	* sem_util.adb (Propagate_Invariant_Attributes): Code clean up.

gcc/testsuite/

	* gnat.dg/assertion_policy1.adb, gnat.dg/assertion_policy1_pkg.adb,
	gnat.dg/assertion_policy1_pkg.ads: New testcase.

From-SVN: r261430

gcc/ada/ChangeLog

 2018-06-11  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* contracts.adb (Process_Body_Postconditions): Expand only checked
+	postconditions.
+	(Process_Contract_Cases_For): Expand only checked contract cases.
+	(Process_Inherited_Preconditions): Ignored class-wide preconditions are
+	partially expanded because some of their semantic checks are tied to
+	the expansion.
+	(Process_Preconditions_For): Expand only checked preconditions.
+	(Process_Spec_Postconditions): Expand only checked preconditions.
+	Ignored class-wide preconditions are partially expanded because some of
+	their semantic checks are tied to the expansion.
+	* exp_prag.adb (Expand_N_Pragma): Suppress the expansion of ignored
+	assertion pragmas.
+	* exp_util.adb (Add_Inherited_Invariants): Code clean up.
+	* sem_util.adb (Propagate_Invariant_Attributes): Code clean up.
+
+2018-06-11  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* exp_ch9.adb, exp_unst.adb, inline.adb, libgnat/a-ciorma.adb,
 	libgnat/a-ciormu.adb, libgnat/a-ciorse.adb, libgnat/a-coorma.adb,
 	libgnat/a-coormu.adb, libgnat/a-coorse.adb, sem_prag.adb: Minor

gcc/ada/contracts.adb

@@ -2284,7 +2284,9 @@ package body Contracts is
             if Present (Items) then
                Prag := Contract_Test_Cases (Items);
                while Present (Prag) loop
-                  if Pragma_Name (Prag) = Name_Contract_Cases then
+                  if Pragma_Name (Prag) = Name_Contract_Cases
+                    and then Is_Checked (Prag)
+                  then
                      Expand_Pragma_Contract_Cases
                        (CCs     => Prag,
                         Subp_Id => Subp_Id,
@@ -2342,7 +2344,9 @@ package body Contracts is
             if Present (Items) then
                Prag := Pre_Post_Conditions (Items);
                while Present (Prag) loop
-                  if Pragma_Name (Prag) = Post_Nam then
+                  if Pragma_Name (Prag) = Post_Nam
+                    and then Is_Checked (Prag)
+                  then
                      Append_Enabled_Item
                        (Item => Build_Pragma_Check_Equivalent (Prag),
                         List => Stmts);
@@ -2364,7 +2368,9 @@ package body Contracts is
                   --  Note that non-matching pragmas are skipped
 
                   if Nkind (Decl) = N_Pragma then
-                     if Pragma_Name (Decl) = Post_Nam then
+                     if Pragma_Name (Decl) = Post_Nam
+                       and then Is_Checked (Decl)
+                     then
                         Append_Enabled_Item
                           (Item => Build_Pragma_Check_Equivalent (Decl),
                            List => Stmts);
@@ -2394,6 +2400,7 @@ package body Contracts is
          procedure Process_Spec_Postconditions is
             Subps   : constant Subprogram_List :=
                         Inherited_Subprograms (Spec_Id);
+            Item    : Node_Id;
             Items   : Node_Id;
             Prag    : Node_Id;
             Subp_Id : Entity_Id;
@@ -2406,7 +2413,9 @@ package body Contracts is
             if Present (Items) then
                Prag := Pre_Post_Conditions (Items);
                while Present (Prag) loop
-                  if Pragma_Name (Prag) = Name_Postcondition then
+                  if Pragma_Name (Prag) = Name_Postcondition
+                    and then Is_Checked (Prag)
+                  then
                      Append_Enabled_Item
                        (Item => Build_Pragma_Check_Equivalent (Prag),
                         List => Stmts);
@@ -2429,13 +2438,20 @@ package body Contracts is
                      if Pragma_Name (Prag) = Name_Postcondition
                        and then Class_Present (Prag)
                      then
-                        Append_Enabled_Item
-                          (Item =>
-                             Build_Pragma_Check_Equivalent
-                               (Prag     => Prag,
-                                Subp_Id  => Spec_Id,
-                                Inher_Id => Subp_Id),
-                           List => Stmts);
+                        Item :=
+                          Build_Pragma_Check_Equivalent
+                            (Prag     => Prag,
+                             Subp_Id  => Spec_Id,
+                             Inher_Id => Subp_Id);
+
+                        --  The pragma Check equivalent of the class-wide
+                        --  postcondition is still created even though the
+                        --  pragma may be ignored because the equivalent
+                        --  performs semantic checks.
+
+                        if Is_Checked (Prag) then
+                           Append_Enabled_Item (Item, Stmts);
+                        end if;
                      end if;
 
                      Prag := Next_Pragma (Prag);
@@ -2630,9 +2646,11 @@ package body Contracts is
          ----------------------
 
          procedure Prepend_To_Decls (Item : Node_Id) is
-            Decls : List_Id := Declarations (Body_Decl);
+            Decls : List_Id;
 
          begin
+            Decls := Declarations (Body_Decl);
+
             --  Ensure that the body has a declarative list
 
             if No (Decls) then
@@ -2680,12 +2698,13 @@ package body Contracts is
          -------------------------------------
 
          procedure Process_Inherited_Preconditions is
-            Subps      : constant Subprogram_List :=
-                           Inherited_Subprograms (Spec_Id);
-            Check_Prag : Node_Id;
-            Items      : Node_Id;
-            Prag       : Node_Id;
-            Subp_Id    : Entity_Id;
+            Subps : constant Subprogram_List :=
+                      Inherited_Subprograms (Spec_Id);
+
+            Item    : Node_Id;
+            Items   : Node_Id;
+            Prag    : Node_Id;
+            Subp_Id : Entity_Id;
 
          begin
             --  Process the contracts of all inherited subprograms, looking for
@@ -2701,20 +2720,29 @@ package body Contracts is
                      if Pragma_Name (Prag) = Name_Precondition
                        and then Class_Present (Prag)
                      then
-                        Check_Prag :=
+                        Item :=
                           Build_Pragma_Check_Equivalent
                             (Prag     => Prag,
                              Subp_Id  => Spec_Id,
                              Inher_Id => Subp_Id);
 
-                        --  The spec of an inherited subprogram already yielded
-                        --  a class-wide precondition. Merge the existing
-                        --  precondition with the current one using "or else".
+                        --  The pragma Check equivalent of the class-wide
+                        --  precondition is still created even though the
+                        --  pragma may be ignored because the equivalent
+                        --  performs semantic checks.
 
-                        if Present (Class_Pre) then
-                           Merge_Preconditions (Check_Prag, Class_Pre);
-                        else
-                           Class_Pre := Check_Prag;
+                        if Is_Checked (Prag) then
+
+                           --  The spec of an inherited subprogram already
+                           --  yielded a class-wide precondition. Merge the
+                           --  existing precondition with the current one
+                           --  using "or else".
+
+                           if Present (Class_Pre) then
+                              Merge_Preconditions (Item, Class_Pre);
+                           else
+                              Class_Pre := Item;
+                           end if;
                         end if;
                      end if;
 
@@ -2736,7 +2764,8 @@ package body Contracts is
          -------------------------------
 
          procedure Process_Preconditions_For (Subp_Id : Entity_Id) is
-            Items     : constant Node_Id := Contract (Subp_Id);
+            Items : constant Node_Id := Contract (Subp_Id);
+
             Decl      : Node_Id;
             Prag      : Node_Id;
             Subp_Decl : Node_Id;
@@ -2747,7 +2776,9 @@ package body Contracts is
             if Present (Items) then
                Prag := Pre_Post_Conditions (Items);
                while Present (Prag) loop
-                  if Pragma_Name (Prag) = Name_Precondition then
+                  if Pragma_Name (Prag) = Name_Precondition
+                    and then Is_Checked (Prag)
+                  then
                      Prepend_To_Decls_Or_Save (Prag);
                   end if;
 
@@ -2772,7 +2803,9 @@ package body Contracts is
                   --  Note that non-matching pragmas are skipped
 
                   if Nkind (Decl) = N_Pragma then
-                     if Pragma_Name (Decl) = Name_Precondition then
+                     if Pragma_Name (Decl) = Name_Precondition
+                       and then Is_Checked (Decl)
+                     then
                         Prepend_To_Decls_Or_Save (Decl);
                      end if;
 
@@ -2908,20 +2941,18 @@ package body Contracts is
 
       elsif Is_Ignored_Ghost_Entity (Subp_Id) then
          return;
-      end if;
 
       --  Do not re-expand the same contract. This scenario occurs when a
       --  construct is rewritten into something else during its analysis
       --  (expression functions for instance).
 
-      if Has_Expanded_Contract (Subp_Id) then
+      elsif Has_Expanded_Contract (Subp_Id) then
          return;
+      end if;
 
-      --  Otherwise mark the subprogram
+      --  Prevent multiple expansion attempts of the same contract
 
-      else
-         Set_Has_Expanded_Contract (Subp_Id);
-      end if;
+      Set_Has_Expanded_Contract (Subp_Id);
 
       --  Ensure that the formal parameters are visible when expanding all
       --  contract items.

gcc/ada/exp_prag.adb

@@ -44,6 +44,7 @@ with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Prag; use Sem_Prag;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 with Sinput;   use Sinput;
@@ -167,11 +168,24 @@ package body Exp_Prag is
       Prag_Id : constant Pragma_Id := Get_Pragma_Id (Pname);
 
    begin
-      --  Rewrite pragma ignored by Ignore_Pragma to null statement, so that
-      --  the back end doesn't see it. The same goes for pragma
-      --  Default_Scalar_Storage_Order if the -gnatI switch was given.
+      --  Suppress the expansion of an ignored assertion pragma. Such a pragma
+      --  should not be transformed into a null statment because:
+      --
+      --    * The pragma may be part of the rep item chain of a type, in which
+      --      case rewriting it will destroy the chain.
+      --
+      --    * The analysis of the pragma may involve two parts (see routines
+      --      Analyze_xxx_In_Decl_Part). The second part of the analysis will
+      --      not happen if the pragma is rewritten.
+
+      if Assertion_Expression_Pragma (Prag_Id) and then Is_Ignored (N) then
+         return;
+
+      --  Rewrite the pragma into a null statement when it is ignored using
+      --  pragma Ignore_Pragma, or denotes Default_Scalar_Storage_Order and
+      --  compilation switch -gnatI is in effect.
 
-      if Should_Ignore_Pragma_Sem (N)
+      elsif Should_Ignore_Pragma_Sem (N)
         or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
                   and then Ignore_Rep_Clauses)
       then

gcc/ada/exp_util.adb

@@ -2307,7 +2307,7 @@ package body Exp_Util is
             Deriv_Typ := T;
          end if;
 
-               pragma Assert (Present (Deriv_Typ));
+         pragma Assert (Present (Deriv_Typ));
 
          --  Determine which rep item chain to use. Precedence is given to that
          --  of the parent type's partial view since it usually carries all the

gcc/ada/sem_util.adb

@@ -23193,19 +23193,19 @@ package body Sem_Util is
          if Has_Inheritable_Invariants (From_Typ)
            and then not Has_Inheritable_Invariants (Typ)
          then
-            Set_Has_Inheritable_Invariants (Typ, True);
+            Set_Has_Inheritable_Invariants (Typ);
          end if;
 
          if Has_Inherited_Invariants (From_Typ)
            and then not Has_Inherited_Invariants (Typ)
          then
-            Set_Has_Inherited_Invariants (Typ, True);
+            Set_Has_Inherited_Invariants (Typ);
          end if;
 
          if Has_Own_Invariants (From_Typ)
            and then not Has_Own_Invariants (Typ)
          then
-            Set_Has_Own_Invariants (Typ, True);
+            Set_Has_Own_Invariants (Typ);
          end if;
 
          if Present (Full_IP) and then No (Invariant_Procedure (Typ)) then

gcc/testsuite/ChangeLog

+2018-06-11  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* gnat.dg/assertion_policy1.adb, gnat.dg/assertion_policy1_pkg.adb,
+	gnat.dg/assertion_policy1_pkg.ads: New testcase.
+
 2018-06-11  Ed Schonberg  <schonberg@adacore.com>
 
 	* gnat.dg/predicate1.adb: New testcase.

gcc/testsuite/gnat.dg/assertion_policy1.adb

+--  { dg-do run }
+--  { dg-options "-gnata" }
+
+with Ada.Text_IO; use Ada.Text_IO;
+with Assertion_Policy1_Pkg; use Assertion_Policy1_Pkg;
+
+procedure Assertion_Policy1 is
+begin
+   Proc (2, 1);
+
+exception
+   when others =>
+      Put_Line ("ERROR: unexpected exception");
+      raise;
+end Assertion_Policy1;

gcc/testsuite/gnat.dg/assertion_policy1_pkg.adb

+with Ada.Text_IO; use Ada.Text_IO;
+
+package body Assertion_Policy1_Pkg is
+   procedure Proc (Low : Integer; High : Integer) is
+   begin
+      Put_Line ("Proc");
+   end Proc;
+end Assertion_Policy1_Pkg;

gcc/testsuite/gnat.dg/assertion_policy1_pkg.ads

+package Assertion_Policy1_Pkg is
+   pragma Assertion_Policy (Ignore);
+
+   procedure Proc (Low : Integer; High : Integer)
+     with Pre => Low < High;
+end Assertion_Policy1_Pkg;