diff options
| author | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-09-25 09:51:49 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-09-25 09:51:49 +0000 |
| commit | 61b1489667e08d7b1ef6672682906072df7bc369 (patch) | |
| tree | c134926fb8862b14d9968c9e1d5623f67a9d56e0 /gcc/ada/sem_ch5.adb | |
| parent | 871a0725ddee3c9ef8cf827cb85ce08e150fec44 (diff) | |
| download | gcc-61b1489667e08d7b1ef6672682906072df7bc369.zip gcc-61b1489667e08d7b1ef6672682906072df7bc369.tar.gz gcc-61b1489667e08d7b1ef6672682906072df7bc369.tar.bz2 | |
[multiple changes]
2017-09-25 Yannick Moy <moy@adacore.com>
* exp_spark.adb (Expand_SPARK_Indexed_Component,
Expand_SPARK_Selected_Component): New procedures to insert explicit
dereference if required.
(Expand_SPARK): Call the new procedures.
2017-09-25 Patrick Bernardi <bernardi@adacore.com>
* libgnat/a-stwiun.adb, libgnat/s-stchop__vxworks.adb,
libgnat/g-socthi__vxworks.ads, libgnat/a-stzunb.adb,
libgnat/a-strunb.adb, libgnarl/s-osinte__lynxos178.adb,
libgnarl/s-intman__vxworks.adb, libgnarl/s-osinte__darwin.adb,
libgnarl/a-exetim__darwin.adb: Removed ineffective use-clauses.
2017-09-25 Vasiliy Fofanov <fofanov@adacore.com>
* adaint.c (win32_wait): Properly handle error and take into account
the WIN32 limitation on the number of simultaneous wait objects.
2017-09-25 Yannick Moy <moy@adacore.com>
* sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the
invariant procedure in GNATprove mode.
* sem_ch5.adb (Analyze_Assignment): Likewise.
From-SVN: r253143
Diffstat (limited to 'gcc/ada/sem_ch5.adb')
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index e72dc4b..d33d59a 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -839,14 +839,16 @@ package body Sem_Ch5 is Set_Referenced_Modified (Lhs, Out_Param => False); end if; - -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type - -- to one of its ancestors) requires an invariant check. Apply check - -- only if expression comes from source, otherwise it will be applied - -- when value is assigned to source entity. + -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type to + -- one of its ancestors) requires an invariant check. Apply check only + -- if expression comes from source, otherwise it will be applied when + -- value is assigned to source entity. This is not done in GNATprove + -- mode, as GNATprove handles invariant checks itself. if Nkind (Lhs) = N_Type_Conversion and then Has_Invariants (Etype (Expression (Lhs))) and then Comes_From_Source (Expression (Lhs)) + and then not GNATprove_Mode then Insert_After (N, Make_Invariant_Call (Expression (Lhs))); end if; |