From: Pierre-Marie de Rodat <derodat@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Yannick Moy <moy@adacore.com>
Subject: [Ada] More precise analysis of function renamings in GNATprove
Date: Wed, 22 Sep 2021 15:15:50 +0000 [thread overview]
Message-ID: <20210922151550.GA1907911@adacore.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 549 bytes --]
When a function renaming has a contract, it is important for GNATprove
that it is not treated as a simple wrapper, otherwise the link between
the renamed function and its renaming is lost for proof. Instead, it
should be treated as an expression function.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* freeze.adb (Build_Renamed_Body): Special case for GNATprove.
* sem_ch6.adb (Analyze_Expression_Function): Remove useless test
for a node to come from source, which becomes harmful otherwise.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 2131 bytes --]
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -636,13 +636,26 @@ package body Freeze is
Next (Param_Spec);
end loop;
- Body_Node :=
- Make_Subprogram_Body (Loc,
- Specification => Spec,
- Declarations => New_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (Call_Node)));
+ -- In GNATprove, prefer to generate an expression function whenever
+ -- possible, to benefit from the more precise analysis in that case
+ -- (as if an implicit postcondition had been generated).
+
+ if GNATprove_Mode
+ and then Nkind (Call_Node) = N_Simple_Return_Statement
+ then
+ Body_Node :=
+ Make_Expression_Function (Loc,
+ Specification => Spec,
+ Expression => Expression (Call_Node));
+ else
+ Body_Node :=
+ Make_Subprogram_Body (Loc,
+ Specification => Spec,
+ Declarations => New_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (Call_Node)));
+ end if;
if Nkind (Decl) /= N_Subprogram_Declaration then
Rewrite (N,
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -385,15 +385,9 @@ package body Sem_Ch6 is
Analyze (New_Body);
Set_Is_Inlined (Prev);
- -- If the expression function is a completion, the previous declaration
- -- must come from source. We know already that it appears in the current
- -- scope. The entity itself may be internally created if within a body
- -- to be inlined.
-
elsif Present (Prev)
and then Is_Overloadable (Prev)
and then not Is_Formal_Subprogram (Prev)
- and then Comes_From_Source (Parent (Prev))
then
Set_Has_Completion (Prev, False);
Set_Is_Inlined (Prev);
reply other threads:[~2021-09-22 15:15 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20210922151550.GA1907911@adacore.com \
--to=derodat@adacore.com \
--cc=gcc-patches@gcc.gnu.org \
--cc=moy@adacore.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).