https://gcc.gnu.org/g:bb80bcec3b81d37f17c4dc8e17c6d437b307911e
commit r16-2757-gbb80bcec3b81d37f17c4dc8e17c6d437b307911e
Author: Viljar Indus <in...@adacore.com>
Date: Wed Jul 16 14:57:51 2025 +0300
ada: Update Assertion_Policy handling in GNATProve mode
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.
Diff:
---
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 70e94874a23f..7e4e4a2077f6 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 0fd668413ac0..e8774699a66a 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 340f2dc10028..7ec963a19508 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 1b2de4f248d8..e9ec7b73d877 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 564f153c9826..92bc3c6029ce 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 52063c8067f7..ee2c329aed7b 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 b7a7f129de95..fb7c4164d622 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 145d314fc3d5..aa9ae57f60eb 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 d2291a9a2c37..bd74215bb967 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 f38380c381f6..78b6318133a4 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 f29690b43f81..31735e41a9c8 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 62ef7560f791..4fd5b658a78d 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 73558c13b89f..d19b3b956223 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 4554f2423e19..47fcc7d14eb0 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
