diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-01-19 14:14:04 +0100 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-01-19 14:14:04 +0100 |
| commit | 332429c807f56de7948885368277723a7a5ac0ac (patch) | |
| tree | 1a9c1687acacfdc07e3eca81776e3635d83c445d /gcc | |
| parent | 7c323fbe3bdff58d4081e4706d24c17f4bb36f8a (diff) | |
| download | gcc-332429c807f56de7948885368277723a7a5ac0ac.zip gcc-332429c807f56de7948885368277723a7a5ac0ac.tar.gz gcc-332429c807f56de7948885368277723a7a5ac0ac.tar.bz2 | |
Code cleanup.
From-SVN: r244634
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/contracts.adb | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index d5b3103..d467c94 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -484,10 +484,13 @@ package body Contracts is -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This -- check is relevant only when SPARK_Mode is on, as it is not a standard -- legality rule. The check is performed here because Volatile_Function - -- is processed after the analysis of the related subprogram body. + -- is processed after the analysis of the related subprogram body. The + -- check only applies to source subprograms and not to generated TSS + -- subprograms. if SPARK_Mode = On and then Ekind_In (Body_Id, E_Function, E_Generic_Function) + and then Comes_From_Source (Spec_Id) and then not Is_Volatile_Function (Body_Id) then Check_Nonvolatile_Function_Profile (Body_Id); |