diff options
| author | Yannick Moy <moy@adacore.com> | 2019-09-19 08:14:03 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-09-19 08:14:03 +0000 |
| commit | 231ef54b96d6022bc844107f50490ba5c96f4a50 (patch) | |
| tree | 34ead3fe4f6594bef2dbb93f2dce6de0f53bf2fa /gcc | |
| parent | 09709b4781192f7724e2bb2977d3610ae727260f (diff) | |
| download | gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.zip gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.tar.gz gcc-231ef54b96d6022bc844107f50490ba5c96f4a50.tar.bz2 | |
[Ada] Disable inlining of traversal function in GNATprove
Traversal functions as defined in SPARK RM 3.10 should not be inlined
for analysis in GNATprove, as this changes the ownership behavior.
Disable the inlining performed in GNATprove on functions which could be
interpreted as such.
There is no impact on compilation and thus no test.
2019-09-19 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add special
case for traversal functions.
From-SVN: r275948
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/inline.adb | 29 |
2 files changed, 34 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 070b8a1..8c88e90 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2019-09-19 Yannick Moy <moy@adacore.com> + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add special + case for traversal functions. + +2019-09-19 Yannick Moy <moy@adacore.com> + * sem_prag.adb (Analyze_Global_In_Decl_Part): Do not issue an error when a constant of an access type is used as output in a Global contract. diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 6e345d6..dab2275 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1512,6 +1512,12 @@ package body Inline is -- Return True if subprogram Id is defined in the package specification, -- either its visible or private part. + function Maybe_Traversal_Function (Id : Entity_Id) return Boolean; + -- Return True if subprogram Id could be a traversal function, as + -- defined in SPARK RM 3.10. This is only a safe approximation, as the + -- knowledge of the SPARK boundary is needed to determine exactly + -- traversal functions. + --------------------------------------------------- -- Has_Formal_With_Discriminant_Dependent_Fields -- --------------------------------------------------- @@ -1635,6 +1641,20 @@ package body Inline is return Nkind (Parent (Decl)) = N_Compilation_Unit; end Is_Unit_Subprogram; + ------------------------------ + -- Maybe_Traversal_Function -- + ------------------------------ + + function Maybe_Traversal_Function (Id : Entity_Id) return Boolean is + begin + return Ekind (Id) = E_Function + + -- Only traversal functions return an anonymous access-to-object + -- type in SPARK. + + and then Is_Anonymous_Access_Type (Etype (Id)); + end Maybe_Traversal_Function; + -- Local declarations Id : Entity_Id; @@ -1757,6 +1777,15 @@ package body Inline is elsif Has_Formal_With_Discriminant_Dependent_Fields (Id) then return False; + -- Do not inline subprograms which may be traversal functions. Such + -- inlining introduces temporary variables of named access type for + -- which assignments are move instead of borrow/observe, possibly + -- leading to spurious errors when checking SPARK rules related to + -- pointer usage. + + elsif Maybe_Traversal_Function (Id) then + return False; + -- Otherwise, this is a subprogram declared inside the private part of a -- package, or inside a package body, or locally in a subprogram, and it -- does not have any contract. Inline it. |