diff options
| author | Yannick Moy <moy@adacore.com> | 2019-12-13 09:03:56 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-12-13 09:03:56 +0000 |
| commit | 2e3795d016a7263c82a4f64a7204f416d12a72da (patch) | |
| tree | 50251f6c4c7b8928e9a446e70b716e274ee54f7c | |
| parent | e841d4d8b3d1e64fe2f31329c8644ceca341874f (diff) | |
| download | gcc-2e3795d016a7263c82a4f64a7204f416d12a72da.zip gcc-2e3795d016a7263c82a4f64a7204f416d12a72da.tar.gz gcc-2e3795d016a7263c82a4f64a7204f416d12a72da.tar.bz2 | |
[Ada] Prevent inlining inside condition of while loop in GNATprove
2019-12-13 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_res.adb (Resolve_Call): Prevent inlining inside while loop
conditions.
* sem_util.adb, sem_util.ads (In_While_Loop_Condition): New
query function.
From-SVN: r279347
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 3 |
4 files changed, 42 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 209a2d4..b5834a9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2019-12-13 Yannick Moy <moy@adacore.com> + + * sem_res.adb (Resolve_Call): Prevent inlining inside while loop + conditions. + * sem_util.adb, sem_util.ads (In_While_Loop_Condition): New + query function. + 2019-12-13 Bob Duff <duff@adacore.com> * impunit.ads: Add Ada_202X_Unit. diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 0bdbc25..11b5316 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7172,6 +7172,14 @@ package body Sem_Res is ("cannot inline & (in potentially unevaluated context)?", N, Nam_UA); + -- Calls cannot be inlined inside the conditions of while + -- loops, as this would create complex actions inside + -- the condition, that are not handled by GNATprove. + + elsif In_While_Loop_Condition (N) then + Cannot_Inline + ("cannot inline & (in while loop condition)?", N, Nam_UA); + -- Do not inline calls which would possibly lead to missing a -- type conversion check on an input parameter. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index ea87a3a..03ce7c0 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -12855,6 +12855,30 @@ package body Sem_Util is and then not In_Private_Part (Scope_Id); end In_Visible_Part; + ----------------------------- + -- In_While_Loop_Condition -- + ----------------------------- + + function In_While_Loop_Condition (N : Node_Id) return Boolean is + Prev : Node_Id := N; + P : Node_Id := Parent (N); + -- P and Prev will be used for traversing the AST, while maintaining an + -- invariant that P = Parent (Prev). + begin + loop + if No (P) then + return False; + elsif Nkind (P) = N_Iteration_Scheme + and then Prev = Condition (P) + then + return True; + else + Prev := P; + P := Parent (P); + end if; + end loop; + end In_While_Loop_Condition; + -------------------------------- -- Incomplete_Or_Partial_View -- -------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index ace843e..ea963de 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1446,6 +1446,9 @@ package Sem_Util is -- package specification. The package must be on the scope stack, and the -- corresponding private part must not. + function In_While_Loop_Condition (N : Node_Id) return Boolean; + -- Returns true if the expression N occurs within the condition of a while + function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id; -- Given the entity of a constant or a type, retrieve the incomplete or -- partial view of the same entity. Note that Id may not have a partial |