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.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Can I get some code review on some Ada SPARK 2014 code?
Date: Thu, 2 Feb 2017 12:52:33 +0100
Organization: A noiseless patient Spider
Message-ID: <o6v6eq$urs$1@dont-email.me>
References: <4c37d9c4-73f0-4a22-8276-8174856cd42e@googlegroups.com>
 <87inoynsgj.fsf@adaheads.sparre-andersen.dk>
 <749b6b39-e444-4f6d-8fa1-7958cfcefc25@googlegroups.com>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 2 Feb 2017 11:50:50 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="318c5d8906de90c8160ea939177e380b";
	logging-data="31612"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19NJ9MLVYpWaraghYEOCehlMgQdBHz8Ztw="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:45.0)
 Gecko/20100101 Thunderbird/45.7.0
In-Reply-To: <749b6b39-e444-4f6d-8fa1-7958cfcefc25@googlegroups.com>
Cancel-Lock: sha1:iPrMPz52D90fw2hstXkO43RJOfU=
Xref: news.eternal-september.org comp.lang.ada:33228
Date: 2017-02-02T12:52:33+01:00
List-Id: <comp.lang.ada>

On 02.02.17 05:00, stevenselectronicmail@gmail.com wrote:

> In Ada SPARK how do I make use of an object composed of multiple protected types?
>
>    type Composed is record
>       A : A_Type;
>       B : B_Type;
>    end record;
>
> if Composed is not Volatile the code does not compile. If Composed is Volatile I cannot pass A and B into subprocedures.

If my understanding of earlier editions of SPARK is still correct,
and applies, it is a good idea to imagine tasks and protected objects
as having rather fixed places in SPARK programs.
So, anything that is reminiscent of moving or creating objects
at run-time (dynamically), in local scopes say, or passing those
things around, won't work.  Rethinking might help, for example,
by finding ways to pass the identity of A and B to subprograms.