[Ada] Calls to protected operations in pre/postcondition

[Arnaud Charlet <charlet at adacore dot com>]

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  <schonberg@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.

Attachment: difs
Description: Text document