diff options
| author | Johannes Kanig <kanig@adacore.com> | 2020-08-17 09:41:10 +0900 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-10-23 04:24:55 -0400 |
| commit | 955886d1a2c75d16b41df1c97d04387bd7436dab (patch) | |
| tree | e1523580cbe7a1b38d6de0e54dec69b7b6c34fff /gcc/ada/exp_util.ads | |
| parent | 294e16b4e7ef586619b92bf0f109448e7de31c6e (diff) | |
| download | gcc-955886d1a2c75d16b41df1c97d04387bd7436dab.zip gcc-955886d1a2c75d16b41df1c97d04387bd7436dab.tar.gz gcc-955886d1a2c75d16b41df1c97d04387bd7436dab.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/exp_util.ads')
| -rw-r--r-- | gcc/ada/exp_util.ads | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index cb288bd..37eb86f 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 |