Contracts for protected objects: internal call cannot appear in precondition of protected operation

[reinert <reinkor@gmail.com>]

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