[gcc r11-4301] [Ada] GNATprove: remove support for external axiomatizations
Pierre-Marie de Rodat
pmderodat@gcc.gnu.org
Fri Oct 23 08:28:02 GMT 2020
https://gcc.gnu.org/g:955886d1a2c75d16b41df1c97d04387bd7436dab
commit r11-4301-g955886d1a2c75d16b41df1c97d04387bd7436dab
Author: Johannes Kanig <kanig@adacore.com>
Date: Mon Aug 17 09:41:10 2020 +0900
[Ada] GNATprove: remove support for external axiomatizations
gcc/ada/
* exp_util.adb, exp_util.ads
(Containing_Package_With_Ext_Axioms,
Has_Annotate_Pragma_For_External_Axiomatizations): Removed.
* sem_ch8.adb (Analyze_Subprogram_Renaming): Removed code
related to external axiomatizations.
* einfo.ads
(Is_Generic_Actual_Subprogram): Removed comment about external
axiomatization.
Diff:
---
gcc/ada/einfo.ads | 4 --
gcc/ada/exp_util.adb | 170 ---------------------------------------------------
gcc/ada/exp_util.ads | 11 ----
gcc/ada/sem_ch8.adb | 34 +----------
4 files changed, 1 insertion(+), 218 deletions(-)
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index da9b49fa5ad..bb5ab07790e 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2655,10 +2655,6 @@ package Einfo is
-- Used to generate constraint checks on calls to these subprograms, even
-- within an instance of a predefined run-time unit, in which checks
-- are otherwise suppressed.
---
--- The flag is also set on the entity of the expression function created
--- within an instance, for a function that has external axiomatization,
--- for use in GNATprove mode.
-- Is_Generic_Actual_Type (Flag94)
-- Defined in all type and subtype entities. Set in the subtype
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 2b05d8acff8..6b474d80f82 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -4615,60 +4615,6 @@ package body Exp_Util is
end if;
end Component_May_Be_Bit_Aligned;
- ----------------------------------------
- -- Containing_Package_With_Ext_Axioms --
- ----------------------------------------
-
- function Containing_Package_With_Ext_Axioms
- (E : Entity_Id) return Entity_Id
- is
- begin
- -- E is the package or generic package which is externally axiomatized
-
- if Is_Package_Or_Generic_Package (E)
- and then Has_Annotate_Pragma_For_External_Axiomatization (E)
- then
- return E;
- end if;
-
- -- If E's scope is axiomatized, E is axiomatized
-
- if Present (Scope (E)) then
- declare
- First_Ax_Parent_Scope : constant Entity_Id :=
- Containing_Package_With_Ext_Axioms (Scope (E));
- begin
- if Present (First_Ax_Parent_Scope) then
- return First_Ax_Parent_Scope;
- end if;
- end;
- end if;
-
- -- Otherwise, if E is a package instance, it is axiomatized if the
- -- corresponding generic package is axiomatized.
-
- if Ekind (E) = E_Package then
- declare
- Par : constant Node_Id := Parent (E);
- Decl : Node_Id;
-
- begin
- if Nkind (Par) = N_Defining_Program_Unit_Name then
- Decl := Parent (Par);
- else
- Decl := Par;
- end if;
-
- if Present (Generic_Parent (Decl)) then
- return
- Containing_Package_With_Ext_Axioms (Generic_Parent (Decl));
- end if;
- end;
- end if;
-
- return Empty;
- end Containing_Package_With_Ext_Axioms;
-
-------------------------------
-- Convert_To_Actual_Subtype --
-------------------------------
@@ -6653,122 +6599,6 @@ package body Exp_Util is
end if;
end Has_Access_Constraint;
- -----------------------------------------------------
- -- Has_Annotate_Pragma_For_External_Axiomatization --
- -----------------------------------------------------
-
- function Has_Annotate_Pragma_For_External_Axiomatization
- (E : Entity_Id) return Boolean
- is
- function Is_Annotate_Pragma_For_External_Axiomatization
- (N : Node_Id) return Boolean;
- -- Returns whether N is
- -- pragma Annotate (GNATprove, External_Axiomatization);
-
- ----------------------------------------------------
- -- Is_Annotate_Pragma_For_External_Axiomatization --
- ----------------------------------------------------
-
- -- The general form of pragma Annotate is
-
- -- pragma Annotate (IDENTIFIER [, IDENTIFIER {, ARG}]);
- -- ARG ::= NAME | EXPRESSION
-
- -- The first two arguments are by convention intended to refer to an
- -- external tool and a tool-specific function. These arguments are
- -- not analyzed.
-
- -- The following is used to annotate a package specification which
- -- GNATprove should treat specially, because the axiomatization of
- -- this unit is given by the user instead of being automatically
- -- generated.
-
- -- pragma Annotate (GNATprove, External_Axiomatization);
-
- function Is_Annotate_Pragma_For_External_Axiomatization
- (N : Node_Id) return Boolean
- is
- Name_GNATprove : constant String :=
- "gnatprove";
- Name_External_Axiomatization : constant String :=
- "external_axiomatization";
- -- Special names
-
- begin
- if Nkind (N) = N_Pragma
- and then Get_Pragma_Id (N) = Pragma_Annotate
- and then List_Length (Pragma_Argument_Associations (N)) = 2
- then
- declare
- Arg1 : constant Node_Id :=
- First (Pragma_Argument_Associations (N));
- Arg2 : constant Node_Id := Next (Arg1);
- Nam1 : Name_Id;
- Nam2 : Name_Id;
-
- begin
- -- Fill in Name_Buffer with Name_GNATprove first, and then with
- -- Name_External_Axiomatization so that Name_Find returns the
- -- corresponding name. This takes care of all possible casings.
-
- Name_Len := 0;
- Add_Str_To_Name_Buffer (Name_GNATprove);
- Nam1 := Name_Find;
-
- Name_Len := 0;
- Add_Str_To_Name_Buffer (Name_External_Axiomatization);
- Nam2 := Name_Find;
-
- return Chars (Get_Pragma_Arg (Arg1)) = Nam1
- and then
- Chars (Get_Pragma_Arg (Arg2)) = Nam2;
- end;
-
- else
- return False;
- end if;
- end Is_Annotate_Pragma_For_External_Axiomatization;
-
- -- Local variables
-
- Decl : Node_Id;
- Vis_Decls : List_Id;
- N : Node_Id;
-
- -- Start of processing for Has_Annotate_Pragma_For_External_Axiomatization
-
- begin
- if Nkind (Parent (E)) = N_Defining_Program_Unit_Name then
- Decl := Parent (Parent (E));
- else
- Decl := Parent (E);
- end if;
-
- Vis_Decls := Visible_Declarations (Decl);
-
- N := First (Vis_Decls);
- while Present (N) loop
-
- -- Skip declarations generated by the frontend. Skip all pragmas
- -- that are not the desired Annotate pragma. Stop the search on
- -- the first non-pragma source declaration.
-
- if Comes_From_Source (N) then
- if Nkind (N) = N_Pragma then
- if Is_Annotate_Pragma_For_External_Axiomatization (N) then
- return True;
- end if;
- else
- return False;
- end if;
- end if;
-
- Next (N);
- end loop;
-
- return False;
- end Has_Annotate_Pragma_For_External_Axiomatization;
-
--------------------
-- Homonym_Number --
--------------------
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index cb288bd0c0e..37eb86fba00 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -427,11 +427,6 @@ package Exp_Util is
-- for trouble using this function and, if so, the assignment is expanded
-- component-wise, which the back end is required to handle correctly.
- function Containing_Package_With_Ext_Axioms
- (E : Entity_Id) return Entity_Id;
- -- Returns the package entity with an external axiomatization containing E,
- -- if any, or Empty if none.
-
procedure Convert_To_Actual_Subtype (Exp : Node_Id);
-- The Etype of an expression is the nominal type of the expression,
-- not the actual subtype. Often these are the same, but not always.
@@ -730,12 +725,6 @@ package Exp_Util is
function Has_Access_Constraint (E : Entity_Id) return Boolean;
-- Given object or type E, determine if a discriminant is of an access type
- function Has_Annotate_Pragma_For_External_Axiomatization
- (E : Entity_Id) return Boolean;
- -- Returns whether E is a package entity, for which the initial list of
- -- pragmas at the start of the package declaration contains
- -- pragma Annotate (GNATprove, External_Axiomatization);
-
function Homonym_Number (Subp : Entity_Id) return Pos;
-- Here subp is the entity for a subprogram. This routine returns the
-- homonym number used to disambiguate overloaded subprograms in the same
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 3bdce445ffa..35c6f60d75d 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -3005,16 +3005,7 @@ package body Sem_Ch8 is
-- Check whether the renaming is for a defaulted actual subprogram
-- with a class-wide actual.
- -- The class-wide wrapper is not needed in GNATprove_Mode and there
- -- is an external axiomatization on the package.
-
- if CW_Actual
- and then Box_Present (Inst_Node)
- and then not
- (GNATprove_Mode
- and then
- Present (Containing_Package_With_Ext_Axioms (Formal_Spec)))
- then
+ if CW_Actual and then Box_Present (Inst_Node) then
Build_Class_Wide_Wrapper (New_S, Old_S);
elsif Is_Entity_Name (Nam)
@@ -3874,29 +3865,6 @@ package body Sem_Ch8 is
Ada_Version_Pragma := Save_AVP;
Ada_Version_Explicit := Save_AV_Exp;
- -- In GNATprove mode, the renamings of actual subprograms are replaced
- -- with wrapper functions that make it easier to propagate axioms to the
- -- points of call within an instance. Wrappers are generated if formal
- -- subprogram is subject to axiomatization.
-
- -- The types in the wrapper profiles are obtained from (instances of)
- -- the types of the formal subprogram.
-
- if Is_Actual
- and then GNATprove_Mode
- and then Present (Containing_Package_With_Ext_Axioms (Formal_Spec))
- and then not Inside_A_Generic
- then
- if Ekind (Old_S) = E_Function then
- Rewrite (N, Build_Function_Wrapper (Formal_Spec, Old_S));
- Analyze (N);
-
- elsif Ekind (Old_S) = E_Operator then
- Rewrite (N, Build_Operator_Wrapper (Formal_Spec, Old_S));
- Analyze (N);
- end if;
- end if;
-
-- Check if we are looking at an Ada 2012 defaulted formal subprogram
-- and mark any use_package_clauses that affect the visibility of the
-- implicit generic actual.
More information about the Gcc-cvs
mailing list