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 --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 70e94874a23fdcb120948fdd6ff5ca2b70a3da3d..7e4e4a2077f6edf22e367480e502420ec10b064f 100644 (file)
--- 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 0fd668413ac0183a31eb92f750ee6dbc5247c749..e8774699a66a6240e98fd8c3e22097a4ef86d9c8 100644 (file)
--- 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 340f2dc10028fcb167d6c2eeb040587c9457e4e3..7ec963a1950813e4e8d35c67dab8c422890c9b76 100644 (file)
--- 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 1b2de4f248d86d42d2f6640580994afd4a004dd0..e9ec7b73d877e9c56950a676ffa74d4f180ee2bf 100644 (file)
--- 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 564f153c9826e21fb5207cc6f8aa928abe63aac7..92bc3c6029ce934d878deea111240885bb20a44f 100644 (file)
--- 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 52063c8067f747304bec8e0d704f3ec79c752d91..ee2c329aed7b7f8e8274fee9d7700fa0a2c15c56 100644 (file)
--- 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 b7a7f129de9597cdf51e368cae00f82ed3a47034..fb7c4164d62251cea7ecb06febe782efa728ddcf 100644 (file)
--- 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 145d314fc3d5444a19c78fb302c08116514557a6..aa9ae57f60eb08c2ec25104c57d2ee8938e2ffad 100644 (file)
--- 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 d2291a9a2c37ad6a410926873448f3990f7deecb..bd74215bb967b1f1074643ad04be1020d8d6460c 100644 (file)
--- 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 f38380c381f6f5cacf5ea04ebffcc5c1c87269dc..78b6318133a4771e4c21b4dbc29b78bb16bf197a 100644 (file)
--- 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 f29690b43f81258ac9ea1f077070a8afa79611f9..31735e41a9c8cb7fde98aa35e8b1b661c74a6c67 100644 (file)
--- 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 62ef7560f7913d937a33fd83c8ac75c209f3bfcd..4fd5b658a78dede8bdcbd261c9455b0d82976f35 100644 (file)
--- 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 73558c13b89ff4cd5831c4bae4b47cc47142850f..d19b3b9562232b71e60148e01736783b25d59522 100644 (file)
--- 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 4554f2423e197d230dd5f5fd40651d2630e8fc2b..47fcc7d14eb07bdc01307d57baa3443db3f3c519 100644 (file)
--- 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