* [Ada] Legality checks on 'Result in the presence of quantified expression
@ 2011-08-01 9:01 Arnaud Charlet
0 siblings, 0 replies; only message in thread
From: Arnaud Charlet @ 2011-08-01 9:01 UTC (permalink / raw)
To: gcc-patches; +Cc: Ed Schonberg
[-- Attachment #1: Type: text/plain, Size: 1161 bytes --]
The expansion of quantified expressions into loops introduces new scopes that
must be taken into account when validating the use of the attribute 'Result.
The following must compile quietly:
gcc -c -gnat12 -gnata test_astrium_2.adb
--
with Ada.Containers.Ordered_Sets;
package Test_Astrium_2 is
package OS is new Ada.Containers.Ordered_Sets
(Element_Type => Integer);
use OS;
function Test_Recovery_Highest (S : Set) return Integer
with Post => (for all Cu in S =>
not (Test_Recovery_Highest'Result < Element (Cu)));
end Test_Astrium_2;
---
package body Test_Astrium_2 is
function Test_Recovery_Highest (S : Set) return Integer is
Res : Integer;
begin
Res := Integer'First;
for Int of S loop
if Int > Res then
Res := Int;
end if;
end loop;
return Res;
end;
end Test_Astrium_2;
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-01 Ed Schonberg <schonberg@adacore.com>
* sem_attr.adb (Analyze_Attribute, case 'Result): Handle properly a
quantified expression that appears within a postcondition and uses the
Ada2012 'Result attribute.
[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1999 bytes --]
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 176998)
+++ sem_attr.adb (working copy)
@@ -3947,14 +3947,29 @@ package body Sem_Attr is
------------
when Attribute_Result => Result : declare
- CS : Entity_Id := Current_Scope;
- PS : Entity_Id := Scope (CS);
+ CS : Entity_Id;
+ -- The enclosing scope, excluding loops for quantified expressions
+
+ PS : Entity_Id;
+ -- During analysis, CS is the postcondition subprogram and PS the
+ -- source subprogram to which the postcondition applies. During
+ -- pre-analysis, CS is the scope of the subprogram declaration.
begin
+ -- Find enclosing scopes, excluding loops
+
+ CS := Current_Scope;
+ while Ekind (CS) = E_Loop loop
+ CS := Scope (CS);
+ end loop;
+
+ PS := Scope (CS);
+
-- If the enclosing subprogram is always inlined, the enclosing
-- postcondition will not be propagated to the expanded call.
- if Has_Pragma_Inline_Always (PS)
+ if not In_Spec_Expression
+ and then Has_Pragma_Inline_Always (PS)
and then Warn_On_Redundant_Constructs
then
Error_Msg_N
@@ -3994,9 +4009,7 @@ package body Sem_Attr is
-- current one.
else
- while Present (CS)
- and then CS /= Standard_Standard
- loop
+ while Present (CS) and then CS /= Standard_Standard loop
if Chars (CS) = Name_uPostconditions then
exit;
else
@@ -4038,7 +4051,7 @@ package body Sem_Attr is
else
Error_Attr
("% attribute can only appear" &
- " in function Postcondition pragma", P);
+ " in function Postcondition pragma", P);
end if;
end if;
end Result;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2011-08-01 9:01 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-08-01 9:01 [Ada] Legality checks on 'Result in the presence of quantified expression Arnaud Charlet
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).