This patch ensures that the boolean expression of pragma Postcondition is
preanalyzed at the point of declaration when the pragma appears inside a
subprogram body.
------------
-- Source --
------------
-- main.adb
procedure Main is
pragma Postcondition (X'Old = 1);
X : Integer := 0;
begin
X := 2;
end Main;
-----------------
-- Compilation --
-----------------
$ gcc -c -gnata main.adb
main.adb:2:26: "X" is undefined
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-01-02 Hristian Kirtchev <kirtc...@adacore.com>
* sem_attr.adb (Analyze_Attribute): Skip the special _Parent
scope generated for subprogram inlining purposes while trying
to locate the enclosing function.
* sem_prag.adb (Analyze_Pragma): Preanalyze the boolean
expression of pragma Postcondition when the pragma comes from
source and appears inside a subprogram body.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 194788)
+++ sem_prag.adb (working copy)
@@ -12748,7 +12748,6 @@
when Pragma_Postcondition => Postcondition : declare
In_Body : Boolean;
- pragma Warnings (Off, In_Body);
begin
GNAT_Pragma;
@@ -12756,10 +12755,22 @@
Check_At_Most_N_Arguments (2);
Check_Optional_Identifier (Arg1, Name_Check);
- -- All we need to do here is call the common check procedure,
- -- the remainder of the processing is found in Sem_Ch6/Sem_Ch7.
+ -- Verify the proper placement of the pragma. The remainder of the
+ -- processing is found in Sem_Ch6/Sem_Ch7.
Check_Precondition_Postcondition (In_Body);
+
+ -- When the pragma is a source contruct and appears inside a body,
+ -- preanalyze the boolean_expression to detect illegal forward
+ -- references:
+
+ -- procedure P is
+ -- pragma Postcondition (X'Old ...);
+ -- X : ...
+
+ if Comes_From_Source (N) and then In_Body then
+ Preanalyze_Spec_Expression (Expression (Arg1), Any_Boolean);
+ end if;
end Postcondition;
------------------
Index: sem_attr.adb
===================================================================
--- sem_attr.adb (revision 194786)
+++ sem_attr.adb (working copy)
@@ -4586,11 +4586,26 @@
-- During pre-analysis, Prag is the enclosing pragma node if any
begin
- -- Find enclosing scopes, excluding loops
+ -- Find the proper enclosing scope
CS := Current_Scope;
- while Ekind (CS) = E_Loop loop
- CS := Scope (CS);
+ while Present (CS) loop
+
+ -- Skip generated loops
+
+ if Ekind (CS) = E_Loop then
+ CS := Scope (CS);
+
+ -- Skip the special _Parent scope generated to capture references
+ -- to formals during the process of subprogram inlining.
+
+ elsif Ekind (CS) = E_Function
+ and then Chars (CS) = Name_uParent
+ then
+ CS := Scope (CS);
+ else
+ exit;
+ end if;
end loop;
PS := Scope (CS);
