Patchwork [Ada] Illegal forward reference in pragma Postcondition

login
register
mail settings
Submitter Arnaud Charlet
Date Jan. 2, 2013, 10:38 a.m.
Message ID <20130102103832.GA19985@adacore.com>
Download mbox | patch
Permalink /patch/208987/
State New
Headers show

Comments

Arnaud Charlet - Jan. 2, 2013, 10:38 a.m.
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  <kirtchev@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.

Patch

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);