From: "G.B." <bauhaus@notmyhomepage.invalid>
Subject: Re: Can I get some code review on some Ada SPARK 2014 code?
Date: Thu, 2 Feb 2017 12:52:33 +0100
Date: 2017-02-02T12:52:33+01:00 [thread overview]
Message-ID: <o6v6eq$urs$1@dont-email.me> (raw)
In-Reply-To: <749b6b39-e444-4f6d-8fa1-7958cfcefc25@googlegroups.com>
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.
prev parent reply other threads:[~2017-02-02 11:52 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-01-29 0:18 Can I get some code review on some Ada SPARK 2014 code? stevenselectronicmail
2017-01-29 9:09 ` Jacob Sparre Andersen
2017-02-02 4:00 ` stevenselectronicmail
2017-02-02 11:52 ` G.B. [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox