diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 15:54:18 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-07-30 15:54:18 +0200 |
| commit | 2178830b048787f68c0b8b7c3dd3d26580a795aa (patch) | |
| tree | 4d659dd4ed85f83c6aebe912ce1e774a2e95d1f2 /gcc/ada/inline.adb | |
| parent | d3e16619ae38fba5a464064046114a6638d1816f (diff) | |
| download | gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.zip gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.tar.gz gcc-2178830b048787f68c0b8b7c3dd3d26580a795aa.tar.bz2 | |
[multiple changes]
2014-07-30 Pat Rogers <rogers@adacore.com>
* gnat_rm.texi: Minor word error.
2014-07-30 Ed Schonberg <schonberg@adacore.com>
* exp_prag.adb (Expand_Old): Insert declarationss of temporaries
created to capture the value of the prefix of 'Old at the
beginning of the current declarative part, to prevent data flow
anomalies in the postcondition procedure that will follow.
2014-07-30 Yannick Moy <moy@adacore.com>
* debug.adb: Retire debug flag -gnatdQ.
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
on decl, not on body. Ignore predicate functions.
* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and
body when generating a decl for a body on which SPARK_Mode aspect
is given.
* sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
attaching pragma to entity, to account for declaration not coming
from source.
* sem_res.adb (Resolve_Call): Issue warning and flag subprogram
as not always inlined in GNATprove mode, when called in an
assertion context.
From-SVN: r213271
Diffstat (limited to 'gcc/ada/inline.adb')
| -rw-r--r-- | gcc/ada/inline.adb | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 4f09958..be556fb 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1692,13 +1692,14 @@ package body Inline is elsif Is_Generic_Instance (Spec_Id) then return False; - -- Only inline subprograms whose body is marked SPARK_Mode On. Other - -- subprogram bodies should not be analyzed. - - elsif Present (Body_Id) - and then (No (SPARK_Pragma (Body_Id)) - or else - Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On) + -- Only inline subprograms whose spec is marked SPARK_Mode On. For + -- the subprogram body, a similar check is performed after the body + -- is analyzed, as this is where a pragma SPARK_Mode might be inserted. + + elsif Present (Spec_Id) + and then (No (SPARK_Pragma (Spec_Id)) + or else + Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On) then return False; @@ -1708,6 +1709,12 @@ package body Inline is elsif Instantiation_Location (Sloc (Id)) /= No_Location then return False; + -- Predicate functions are treated specially by GNATprove. Do not inline + -- them. + + elsif Is_Predicate_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. |