From: Viljar Indus <in...@adacore.com>
Previously in GNATProve_Mode the frontend would overwrite all of
the assertion policies to check in order to force the generation
of all of the assertions.
This however prevents GNATProve from performing policy related
checks in the tool. Since they are all artificially changed to
check.
This patch removes the modifications to the applicable assertion
policies and instead prevents code from ignored entities being
removed when in GNATProve_Mode.
gcc/ada/ChangeLog:
* contracts.adb: Use Is_Ignored_In_Codegen instead of just
using Is_Ignored.
* exp_ch6.adb: Likewise.
* exp_prag.adb: Likewise.
* exp_util.adb: Likewise.
* frontend.adb: Avoid removal of ignored nodes in GNATProve_Mode.
* gnat1drv.adb: Avoid forcing Assertions_Enabled in GNATProve_Mode.
* lib-writ.adb (Write_With_File_Names): Avoid early exit
with ignored entities in GNATProve_Mode.
* lib-xref.adb: Likewise.
* opt.adb: Remove check for Assertions_Enabled.
* sem_attr.adb: Use Is_Ignored_In_Codegen instead of Is_Ignored.
* sem_ch13.adb: Likewise. Additionally always add predicates in
GNATProve_Mode.
* sem_prag.adb: Likewise. Additionally remove modifications
to applied policies in GNATProve_Mode.
* sem_util.adb (Is_Ignored_In_Codegen): New function that overrides
Is_Ignored in GNATProve_Mode and Codepeer_Mode.
(Is_Ignored_Ghost_Pragma_In_Codegen): Likewise for
Is_Ignored_Ghost_Pragma.
(Is_Ignored_Ghost_Entity_In_Codegen): Likewise for
Is_Ignored_Ghost_Entity.
(Policy_In_List): Remove overriding of policies in GNATProve_Mode.
* sem_util.ads: Add specs for new functions.
* (Predicates_Enabled): Always generate predicates in
GNATProve_Mode.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/contracts.adb | 5 ++--
gcc/ada/exp_ch6.adb | 2 +-
gcc/ada/exp_prag.adb | 16 +++++++------
gcc/ada/exp_util.adb | 4 ++--
gcc/ada/frontend.adb | 2 +-
gcc/ada/gnat1drv.adb | 5 ----
gcc/ada/lib-writ.adb | 2 +-
gcc/ada/lib-xref.adb | 4 ++--
gcc/ada/opt.adb | 9 +-------
gcc/ada/sem_attr.adb | 2 +-
gcc/ada/sem_ch13.adb | 9 ++++----
gcc/ada/sem_prag.adb | 39 ++++++++-----------------------
gcc/ada/sem_util.adb | 53 ++++++++++++++++++++++++++++++++-----------
gcc/ada/sem_util.ads | 12 ++++++++++
14 files changed, 87 insertions(+), 77 deletions(-)
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 70e94874a23..7e4e4a2077f 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -2714,10 +2714,11 @@ package body Contracts is
procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
begin
- -- Do not chain ignored or disabled pragmas
+ -- Do not chain ignored or disabled pragmas. Note that disabled
+ -- pragmas are also considered ignored.
if Nkind (Item) = N_Pragma
- and then (Is_Ignored (Item) or else Is_Disabled (Item))
+ and then Is_Ignored_In_Codegen (Item)
then
null;
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 0fd668413ac..e8774699a66 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -8099,7 +8099,7 @@ package body Exp_Ch6 is
Get_Class_Wide_Pragma (Id, Pragma_Precondition);
begin
- if No (Prag) or else Is_Ignored (Prag) then
+ if No (Prag) or else Is_Ignored_In_Codegen (Prag) then
return;
end if;
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index 340f2dc1002..7ec963a1950 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -134,7 +134,9 @@ package body Exp_Prag is
-- 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
+ if Assertion_Expression_Pragma (Prag_Id)
+ and then Is_Ignored_In_Codegen (N)
+ then
return;
-- Rewrite the pragma into a null statement when it is ignored using
@@ -143,7 +145,7 @@ package body Exp_Prag is
elsif Should_Ignore_Pragma_Sem (N)
or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
- and then Ignore_Rep_Clauses)
+ and then Ignore_Rep_Clauses)
then
Rewrite (N, Make_Null_Statement (Sloc (N)));
return;
@@ -480,7 +482,7 @@ package body Exp_Prag is
begin
-- Nothing to do if pragma is ignored
- if Is_Ignored (N) then
+ if Is_Ignored_In_Codegen (N) then
return;
end if;
@@ -1837,7 +1839,7 @@ package body Exp_Prag is
-- Do nothing if pragma is not enabled. If pragma is disabled, it has
-- already been rewritten as a Null statement.
- if Is_Ignored (CCs) then
+ if Is_Ignored_In_Codegen (CCs) then
return;
-- Guard against malformed contract cases
@@ -2538,7 +2540,7 @@ package body Exp_Prag is
-- Nothing to do when the pragma is ignored because its semantics are
-- suppressed.
- if Is_Ignored (IC_Prag) then
+ if Is_Ignored_In_Codegen (IC_Prag) then
return;
-- Nothing to do when the pragma or its argument are illegal because
@@ -3001,7 +3003,7 @@ package body Exp_Prag is
-- Also do this in CodePeer mode, because the expanded code is too
-- complicated for CodePeer to analyse.
- if Is_Ignored (N)
+ if Is_Ignored_In_Codegen (N)
or else Chars (Last_Var) = Name_Structural
or else CodePeer_Mode
then
@@ -3391,7 +3393,7 @@ package body Exp_Prag is
-- Do nothing if pragma is not present or is disabled.
-- Also ignore structural variants for execution.
- if Is_Ignored (Prag)
+ if Is_Ignored_In_Codegen (Prag)
or else Chars (Nlists.Last (Choices (Last_Variant))) = Name_Structural
then
return;
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 1b2de4f248d..e9ec7b73d87 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1903,7 +1903,7 @@ package body Exp_Util is
begin
-- The DIC pragma is ignored, nothing left to do
- if Is_Ignored (DIC_Prag) then
+ if Is_Ignored_In_Codegen (DIC_Prag) then
null;
-- Otherwise the DIC expression must be checked at run time.
@@ -3235,7 +3235,7 @@ package body Exp_Util is
begin
-- The invariant is ignored, nothing left to do
- if Is_Ignored (Prag) then
+ if Is_Ignored_In_Codegen (Prag) then
null;
-- Otherwise the invariant is checked. Build a pragma Check to verify
diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index 564f153c982..92bc3c6029c 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -477,7 +477,7 @@ begin
-- executable. This action must be performed very late because it
-- heavily alters the tree.
- if Operating_Mode = Generate_Code or else GNATprove_Mode then
+ if Operating_Mode = Generate_Code and not CodePeer_Mode then
Remove_Ignored_Ghost_Code;
end if;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 52063c8067f..ee2c329aed7 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -503,11 +503,6 @@ procedure Gnat1drv is
Operating_Mode := Check_Semantics;
- -- Enable assertions, since they give valuable extra information for
- -- formal verification.
-
- Assertions_Enabled := True;
-
-- Disable validity checks, since it generates code raising
-- exceptions for invalid data, which confuses GNATprove. Invalid
-- data is directly detected by GNATprove's flow analysis.
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb
index b7a7f129de9..fb7c4164d62 100644
--- a/gcc/ada/lib-writ.adb
+++ b/gcc/ada/lib-writ.adb
@@ -905,7 +905,7 @@ package body Lib.Writ is
-- Do not generate a with line for an ignored Ghost unit because
-- the unit does not have an ALI file.
- if Is_Ignored_Ghost_Entity (Cunit_Entity (Unum)) then
+ if Is_Ignored_Ghost_Entity_In_Codegen (Cunit_Entity (Unum)) then
goto Next_With_Line;
end if;
diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index 145d314fc3d..aa9ae57f60e 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -1729,7 +1729,7 @@ package body Lib.Xref is
-- entity because neither the entity nor its references will
-- appear in the final tree.
- if Is_Ignored_Ghost_Entity (Ent) then
+ if Is_Ignored_Ghost_Entity_In_Codegen (Ent) then
goto Orphan_Continue;
end if;
@@ -2190,7 +2190,7 @@ package body Lib.Xref is
-- entity because neither the entity nor its references will
-- appear in the final tree.
- if Is_Ignored_Ghost_Entity (Ent) then
+ if Is_Ignored_Ghost_Entity_In_Codegen (Ent) then
goto Continue;
end if;
diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb
index d2291a9a2c3..bd74215bb96 100644
--- a/gcc/ada/opt.adb
+++ b/gcc/ada/opt.adb
@@ -204,14 +204,7 @@ package body Opt is
SPARK_Mode_Pragma := SPARK_Mode_Pragma_Config;
else
- -- In GNATprove mode assertions should be always enabled, even
- -- when analysing internal units.
-
- if GNATprove_Mode then
- pragma Assert (Assertions_Enabled);
- null;
-
- elsif GNAT_Mode_Config then
+ if GNAT_Mode_Config then
Assertions_Enabled := Assertions_Enabled_Config;
else
Assertions_Enabled := False;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index f38380c381f..78b6318133a 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -5092,7 +5092,7 @@ package body Sem_Attr is
-- early transformation also avoids the generation of a useless loop
-- entry constant.
- if Present (Encl_Prag) and then Is_Ignored (Encl_Prag) then
+ if Present (Encl_Prag) and then Is_Ignored_In_Codegen (Encl_Prag) then
Rewrite (N, Relocate_Node (P));
Preanalyze_And_Resolve (N);
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f29690b43f8..31735e41a9c 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -4799,7 +4799,7 @@ package body Sem_Ch13 is
and then not Is_Ignored_Ghost_Entity (E)
then
if A_Id = Aspect_Pre then
- if Is_Ignored (Aspect) then
+ if Is_Ignored_In_Codegen (Aspect) then
Set_Ignored_Class_Preconditions (E,
New_Copy_Tree (Expr));
else
@@ -4813,7 +4813,7 @@ package body Sem_Ch13 is
elsif No (Class_Postconditions (E))
and then No (Ignored_Class_Postconditions (E))
then
- if Is_Ignored (Aspect) then
+ if Is_Ignored_In_Codegen (Aspect) then
Set_Ignored_Class_Postconditions (E,
New_Copy_Tree (Expr));
else
@@ -10448,7 +10448,7 @@ package body Sem_Ch13 is
-- which is needed to generate the corresponding predicate
-- function.
- if Is_Ignored_Ghost_Pragma (Prag) then
+ if Is_Ignored_Ghost_Pragma_In_Codegen (Prag) then
Add_Condition (New_Occurrence_Of (Standard_True, Sloc (Prag)));
else
@@ -10489,7 +10489,8 @@ package body Sem_Ch13 is
-- "and"-in the Arg2 condition to evolving expression
- if not Is_Ignored_Ghost_Pragma (Prag) then
+ if not Is_Ignored_Ghost_Pragma_In_Codegen (Prag)
+ then
Add_Condition (Arg2_Copy);
end if;
end;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 62ef7560f79..4fd5b658a78 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5761,7 +5761,7 @@ package body Sem_Prag is
begin
if Pname = Name_Pre_Class then
- if Is_Ignored (N) then
+ if Is_Ignored_In_Codegen (N) then
Set_Ignored_Class_Preconditions (Subp_Id,
New_Copy_Tree (Expr));
else
@@ -5769,7 +5769,7 @@ package body Sem_Prag is
end if;
else
- if Is_Ignored (N) then
+ if Is_Ignored_In_Codegen (N) then
Set_Ignored_Class_Postconditions (Subp_Id,
New_Copy_Tree (Expr));
else
@@ -14868,18 +14868,9 @@ package body Sem_Prag is
Set_Is_Ignored (N, False);
else
- -- In CodePeer mode and GNATprove mode, we need to
- -- consider all assertions, unless they are disabled,
- -- because transformations of the AST may depend on
- -- assertions being checked.
+ Set_Is_Checked (N, False);
+ Set_Is_Ignored (N, True);
- if CodePeer_Mode or GNATprove_Mode then
- Set_Is_Checked (N, True);
- Set_Is_Ignored (N, False);
- else
- Set_Is_Checked (N, False);
- Set_Is_Ignored (N, True);
- end if;
end if;
end Handle_Dynamic_Predicate_Check;
@@ -15043,7 +15034,7 @@ package body Sem_Prag is
-- False at compile time, and we do not want to delete this
-- warning when we delete the if statement.
- if Expander_Active and Is_Ignored (N) then
+ if Expander_Active and Is_Ignored_In_Codegen (N) then
Eloc := Sloc (Expr);
Rewrite (N,
@@ -16242,10 +16233,10 @@ package body Sem_Prag is
Cond :=
New_Occurrence_Of
(Boolean_Literals
- (Expander_Active and then not Is_Ignored (N)),
+ (Expander_Active and then not Is_Ignored_In_Codegen (N)),
Loc);
- if not Is_Ignored (N) then
+ if not Is_Ignored_In_Codegen (N) then
Set_SCO_Pragma_Enabled (Loc);
end if;
@@ -32188,20 +32179,8 @@ package body Sem_Prag is
when Name_Ignore
| Name_Off
=>
- -- In CodePeer mode and GNATprove mode, we need to
- -- consider all assertions, unless they are disabled.
- -- Force Is_Checked on ignored assertions, in particular
- -- because transformations of the AST may depend on
- -- assertions being checked (e.g. the translation of
- -- attribute 'Loop_Entry).
-
- if CodePeer_Mode or GNATprove_Mode then
- Set_Is_Checked (N, True);
- Set_Is_Ignored (N, False);
- else
- Set_Is_Checked (N, False);
- Set_Is_Ignored (N, True);
- end if;
+ Set_Is_Checked (N, False);
+ Set_Is_Ignored (N, True);
when Name_Check
| Name_On
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 73558c13b89..d19b3b95622 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12472,6 +12472,41 @@ package body Sem_Util is
end if;
end Is_Extended_Access_Type;
+ ----------------------------------------
+ -- Is_Ignored_Ghost_Entity_In_Codegen --
+ ----------------------------------------
+
+ function Is_Ignored_Ghost_Entity_In_Codegen (N : Entity_Id) return Boolean
+ is
+ begin
+ return
+ Is_Ignored_Ghost_Entity (N)
+ and then not GNATprove_Mode
+ and then not CodePeer_Mode;
+ end Is_Ignored_Ghost_Entity_In_Codegen;
+
+ ----------------------------------------
+ -- Is_Ignored_Ghost_Pragma_In_Codegen --
+ ----------------------------------------
+
+ function Is_Ignored_Ghost_Pragma_In_Codegen (N : Node_Id) return Boolean is
+ begin
+ return
+ Is_Ignored_Ghost_Pragma (N)
+ and then not GNATprove_Mode
+ and then not CodePeer_Mode;
+ end Is_Ignored_Ghost_Pragma_In_Codegen;
+
+ ---------------------------
+ -- Is_Ignored_In_Codegen --
+ ---------------------------
+
+ function Is_Ignored_In_Codegen (N : Node_Id) return Boolean is
+ begin
+ return
+ Is_Ignored (N) and then not GNATprove_Mode and then not CodePeer_Mode;
+ end Is_Ignored_In_Codegen;
+
---------------------------------
-- Side_Effect_Free_Statements --
---------------------------------
@@ -26438,16 +26473,6 @@ package body Sem_Util is
end if;
end if;
- -- In CodePeer mode and GNATprove mode, we need to consider all
- -- assertions, unless they are disabled. Force Name_Check on
- -- ignored assertions.
-
- if Kind in Name_Ignore | Name_Off
- and then (CodePeer_Mode or GNATprove_Mode)
- then
- Kind := Name_Check;
- end if;
-
return Kind;
end Policy_In_Effect;
@@ -26481,9 +26506,11 @@ package body Sem_Util is
function Predicate_Enabled (Typ : Entity_Id) return Boolean is
begin
- return Present (Predicate_Function (Typ))
- and then not Predicates_Ignored (Typ)
- and then not Predicate_Checks_Suppressed (Empty);
+ return
+ Present (Predicate_Function (Typ))
+ and then (GNATprove_Mode
+ or else (not Predicates_Ignored (Typ)
+ and then not Predicate_Checks_Suppressed (Empty)));
end Predicate_Enabled;
----------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 4554f2423e1..47fcc7d14eb 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2079,6 +2079,18 @@ package Sem_Util is
-- . machine_emax = 2**14
-- . machine_emin = 3 - machine_emax
+ function Is_Ignored_Ghost_Entity_In_Codegen (N : Node_Id) return Boolean;
+ -- True if N Is_Ignored_Ghost_Entity and GNATProve_mode and Codepeer_Mode
+ -- are not active.
+
+ function Is_Ignored_Ghost_Pragma_In_Codegen (N : Node_Id) return Boolean;
+ -- True if N Is_Ignored_Ghost_Pragma and GNATProve_mode and Codepeer_Mode
+ -- are not active.
+
+ function Is_Ignored_In_Codegen (N : Node_Id) return Boolean;
+ -- True if N Is_Ignored and GNATProve_mode and Codepeer_Mode are not
+ -- active.
+
function Is_EVF_Expression (N : Node_Id) return Boolean;
-- Determine whether node N denotes a reference to a formal parameter of
-- a specific tagged type whose related subprogram is subject to pragma
--
2.43.0
