[Ada] Preconditions and Postconditions on generic subprograms.

Arnaud Charlet charlet@adacore.com
Thu Jul 31 11:37:00 GMT 2008


This patch extends the use of pre- and postconditions to generic procedures
and functions. The checks are applied to every instance of the generic unit,
with the same visibility rules.

Executing:
   gnatmake -q -gnat05 genericppcm
   genericppcm

must yield:

   preconditionn violated in call
   postcondition violated in call
---
with genericppc;
with system.assertions; use system.assertions;
with text_io; use text_io;
procedure genericppcm is
   function g is new genericppc (integer);
   x : integer;
begin
   begin
      x := g (-1, -3);
      Put_Line (X'Img);
   exception
      when Assert_Failure =>
         Put_Line ("precondition violated in call");
   end;
   begin
      x := g (-1, -3);
      Put_Line (X'Img);
   exception
      when Assert_Failure =>
         Put_Line ("postcondition violated in call");
   end;
end;
---
generic
   type T_Item is private;
function genericppc (T : in t_Item; I : integer) return integer;
pragma Precondition (I > -2);
pragma Postcondition (genericppc'result > 0);
---
function genericppc (T : in t_Item; I : integer) return integer is
begin
   return -1;
end;

Tested on i686-pc-linux-gnu, committed on trunk


2008-07-31  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb (Analyze_Generic_Subprogram_Body): After analysis,
	transfer pre/postconditions from generic copy to original tree, so that
	they will appear in each instance.
	(Process_PPCs): Do not transform postconditions into a procedure in a
	generic context, to prevent double expansion of check pragmas.
	
	* sem_attr.adb: In an instance, the prefix of the 'result attribute
	can be the renaming of the
	current instance, so check validity of the name accordingly.

-------------- next part --------------
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 138364)
+++ sem_attr.adb	(working copy)
@@ -3739,21 +3739,17 @@ package body Sem_Attr is
 
       when Attribute_Result => Result : declare
          CS : constant Entity_Id := Current_Scope;
-         PS : Entity_Id;
+         PS : constant Entity_Id := Scope (CS);
 
       begin
-         PS := Scope (CS);
+         --  If the enclosing subprogram is always inlined, the enclosing
+         --  postcondition will not be propagated to the expanded call.
 
-         --  If we are analyzing a body to be inlined, there is an additional
-         --  scope present, used to gather global references. Retrieve the
-         --  source scope.
-
-         if Chars (PS) = Name_uParent then
-            PS := Scope (PS);
-            if Warn_On_Redundant_Constructs then
-               Error_Msg_N
-                 ("postconditions on inlined functions not enforced", N);
-            end if;
+         if Has_Pragma_Inline_Always (PS)
+           and then Warn_On_Redundant_Constructs
+         then
+            Error_Msg_N
+              ("postconditions on inlined functions not enforced?", N);
          end if;
 
          --  If we are in the scope of a function and in Spec_Expression mode,
@@ -3796,6 +3792,16 @@ package body Sem_Attr is
             then
                null;
 
+            --  Within an instance, the prefix designates the local renaming
+            --  of the original generic.
+
+            elsif Is_Entity_Name (P)
+              and then Ekind (Entity (P)) = E_Function
+              and then Present (Alias (Entity (P)))
+              and then Chars (Alias (Entity (P))) = Chars (PS)
+            then
+               null;
+
             else
                Error_Msg_NE
                  ("incorrect prefix for % attribute, expected &", P, PS);
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 138355)
+++ sem_ch6.adb	(working copy)
@@ -891,6 +891,37 @@ package body Sem_Ch6 is
          end if;
 
          Set_Actual_Subtypes (N, Current_Scope);
+         Process_PPCs (N, Gen_Id, Body_Id);
+
+         --  If the generic unit carries pre- or post-conditions, copy them
+         --  to the original generic tree, so that they are properly added
+         --  to any instantiation.
+
+         declare
+            Orig : constant Node_Id := Original_Node (N);
+            Cond : Node_Id;
+
+         begin
+            Cond := First (Declarations (N));
+            while Present (Cond) loop
+               if Nkind (Cond) = N_Pragma
+                 and then Pragma_Name (Cond) = Name_Check
+               then
+                  Prepend (New_Copy_Tree (Cond), Declarations (Orig));
+
+               elsif Nkind (Cond) = N_Pragma
+                 and then Pragma_Name (Cond) = Name_Postcondition
+               then
+                  Set_Ekind (Defining_Entity (Orig), Ekind (Gen_Id));
+                  Prepend (New_Copy_Tree (Cond), Declarations (Orig));
+               else
+                  exit;
+               end if;
+
+               Next (Cond);
+            end loop;
+         end;
+
          Analyze_Declarations (Declarations (N));
          Check_Completion;
          Analyze (Handled_Statement_Sequence (N));
@@ -1874,6 +1905,10 @@ package body Sem_Ch6 is
          end if;
       end if;
 
+      if Chars (Body_Id) = Name_uPostconditions then
+         Set_Has_Postconditions (Current_Scope);
+      end if;
+
       --  Place subprogram on scope stack, and make formals visible. If there
       --  is a spec, the visible entity remains that of the spec.
 
@@ -7752,9 +7787,17 @@ package body Sem_Ch6 is
          --  procedure. Note that it is only at the outer level that we
          --  do this fiddling, for the spec cases, the already preanalyzed
          --  parameters are not affected.
+         --  For a postcondition pragma within a generic, preserve the pragma
+         --  for later expansion.
 
          Set_Analyzed (CP, False);
 
+         if Nam = Name_Postcondition
+           and then not Expander_Active
+         then
+            return CP;
+         end if;
+
          --  Change pragma into corresponding pragma Check
 
          Prepend_To (Pragma_Argument_Associations (CP),
@@ -7827,7 +7870,15 @@ package body Sem_Ch6 is
                   end if;
 
                   Analyze (Prag);
-                  Append (Grab_PPC (Name_Postcondition), Plist);
+
+                  --  If expansion is disabled, as in a generic unit,
+                  --  save pragma for later expansion.
+
+                  if not Expander_Active then
+                     Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+                  else
+                     Append (Grab_PPC (Name_Postcondition), Plist);
+                  end if;
                end if;
 
                Next (Prag);
@@ -7860,16 +7911,23 @@ package body Sem_Ch6 is
                   Plist := Empty_List;
                end if;
 
-               Append (Grab_PPC (Name_Postcondition), Plist);
+               if not Expander_Active then
+                  Prepend (Grab_PPC (Name_Postcondition), Declarations (N));
+               else
+                  Append (Grab_PPC (Name_Postcondition), Plist);
+               end if;
             end if;
 
             Prag := Next_Pragma (Prag);
          end loop;
       end if;
 
-      --  If we had any postconditions, build the procedure
+      --  If we had any postconditions and expansion is enabled,, build
+      --  the Postconditions procedure.
 
-      if Present (Plist) then
+      if Present (Plist)
+        and then Expander_Active
+      then
          Subp := Defining_Entity (N);
 
          if Etype (Subp) /= Standard_Void_Type then


More information about the Gcc-patches mailing list