[Ada] Calls to protected operations in pre/postcondition

[Arnaud Charlet]

A protected specification cannot contain calls to its own operations, except
if the call appears within a pre- or postcondition for another protected
operation.

Executing:

   gnatmake -q -gnata prot
   prot

must yield:

   Good call
   Bad call


---
with Text_IO; use Text_IO;
with Ada.Assertions;  use Ada.Assertions;
procedure Prot is

   protected T is
      procedure Set;
      function Is_Empty return Boolean; --   is (True);

      procedure Pop (V : out Integer)
         with Pre => not Is_Empty, Post => V > 10;

   private
      Empty : Boolean := True;
   end T;

   protected body T is
      procedure Set is
      begin
         Empty := False;
      end;

      function Is_Empty return Boolean is
      begin
         return Empty;
      end Is_Empty;

      procedure Pop (V : out Integer) is
      begin
         V := 20;
         Empty := True;
      end Pop;

   end T;
   Counter : Integer := 0;
begin
   T.Set;
   T.Pop (Counter);
   Put_Line ("Good call");

   begin
      T.Pop (Counter);
   exception
      when Assertion_Error => Put_Line ("Bad call");
   end;
end Prot;

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

2014-10-31  Ed Schonberg  <schonb...@adacore.com>

        * sem_res.adb (Resolve_Call): Do not reject a call to a protected
        operation in the spec of a protected type, when the call appears
        in a pre/postcondition for another protected operation.


Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 216925)
+++ sem_res.adb (working copy)
@@ -6022,11 +6022,13 @@
       end if;
 
       --  A protected function cannot be called within the definition of the
-      --  enclosing protected type.
+      --  enclosing protected type, unless it is part of a pre/postcondition
+      --  on another protected operation.
 
       if Is_Protected_Type (Scope (Nam))
         and then In_Open_Scopes (Scope (Nam))
         and then not Has_Completion (Scope (Nam))
+        and then not In_Spec_Expression
       then
          Error_Msg_NE
            ("& cannot be called before end of protected definition", N, Nam);