From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Received: by 2002:aed:2496:: with SMTP id t22mr23150957qtc.2.1590298021119;
        Sat, 23 May 2020 22:27:01 -0700 (PDT)
X-Received: by 2002:a9d:4e88:: with SMTP id v8mr15633607otk.276.1590298020884;
 Sat, 23 May 2020 22:27:00 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sat, 23 May 2020 22:27:00 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: google-groups.googlegroups.com; posting-host=212.251.152.55;
 posting-account=bPTmZAoAAAC_6HP9XLKB9aAAxBa6BuOR
NNTP-Posting-Host: 212.251.152.55
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4ed8fa1e-0b4d-4d6b-bc36-0236f6965db0@googlegroups.com>
Subject: Contracts for protected objects: internal call cannot appear in
 precondition of protected operation
From: reinert <reinkor@gmail.com>
Injection-Date: Sun, 24 May 2020 05:27:01 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader01.eternal-september.org comp.lang.ada:58770
Date: 2020-05-23T22:27:00-07:00
List-Id: <comp.lang.ada>

Hello,

I tried to use pre-conditions for an entry in a protected object.
Say (in the specification):

   entry E1 with Pre => test1;   

This seems OK when test1 is external (defined outside the protected object).

However, when test1 is defined inside the protected object, I get:

internal call cannot appear in precondition of protected operation

(I assume this is related to avoid deadlock - but testing from outside
here should not give deadlock?)

I also would like to include (for security) a test on a variable
defined in the private part of the protected object). Anyhow possible?
I do not mange to include pre/post conditions in the body of my
protected object. I missed something?

reinert