diff options
| author | Yannick Moy <moy@adacore.com> | 2018-05-28 08:52:53 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-28 08:52:53 +0000 |
| commit | e740ff85bd5f9924128d67db1bb66b6a0ba23518 (patch) | |
| tree | 7f0c72a8f67cb40e274d883fd8933377aee44529 /gcc | |
| parent | 7672ab42ccdedf12b8bab23309e86e7a393e9d99 (diff) | |
| download | gcc-e740ff85bd5f9924128d67db1bb66b6a0ba23518.zip gcc-e740ff85bd5f9924128d67db1bb66b6a0ba23518.tar.gz gcc-e740ff85bd5f9924128d67db1bb66b6a0ba23518.tar.bz2 | |
[Ada] Further evaluation of type bounds in GNATprove mode
Some static bounds of types are not recognized and evaluated as such in the
semantic analysis phase of the frontend, which leads to incomplete information
in GNATprove. Fix that in the GNATprove mode only, as this is not needed when
full expansion is used.
There is no impact on compilation.
2018-05-28 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_res.adb (Resolve_Range): Re-resolve the low bound of a range in
GNATprove mode, as the order of resolution (low then high) means that
all the information is not available when resolving the low bound the
first time.
From-SVN: r260816
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 7 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 11 |
2 files changed, 18 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 41df33f..b1ccf57 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-05-28 Yannick Moy <moy@adacore.com> + + * sem_res.adb (Resolve_Range): Re-resolve the low bound of a range in + GNATprove mode, as the order of resolution (low then high) means that + all the information is not available when resolving the low bound the + first time. + 2018-05-28 Eric Botcazou <ebotcazou@adacore.com> * repinfo.adb (List_Array_Info): Start with an explicit blank line and diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d11296c..f0b77c1 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -9800,6 +9800,17 @@ package body Sem_Res is Resolve (L, Typ); Resolve (H, Base_Type (Typ)); + -- Reanalyze the lower bound after both bounds have been analyzed, so + -- that the range is known to be static or not by now. This may trigger + -- more compile-time evaluation, which is useful for static analysis + -- with GNATprove. This is not needed for compilation or static analysis + -- with CodePeer, as full expansion does that evaluation then. + + if GNATprove_Mode then + Set_Analyzed (L, False); + Resolve (L, Typ); + end if; + -- Check for inappropriate range on unordered enumeration type if Bad_Unordered_Enumeration_Reference (N, Typ) |