This patch suppresses the expansion of ignored assertion pragmas.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-06-11 Hristian Kirtchev <kirtc...@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.--- gcc/ada/contracts.adb
+++ 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
+++ 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
+++ 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
+++ 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
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/assertion_policy1.adb
@@ -0,0 +1,15 @@
+-- { 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;
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/assertion_policy1_pkg.adb
@@ -0,0 +1,8 @@
+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;
--- /dev/null
new file mode 100644
+++ gcc/testsuite/gnat.dg/assertion_policy1_pkg.ads
@@ -0,0 +1,6 @@
+package Assertion_Policy1_Pkg is
+ pragma Assertion_Policy (Ignore);
+
+ procedure Proc (Low : Integer; High : Integer)
+ with Pre => Low < High;
+end Assertion_Policy1_Pkg;
