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=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable 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: "Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org>
Newsgroups: comp.lang.ada
Subject: Re: Rust's temporal safety for Ada/SPARK
Date: Mon, 15 May 2017 21:30:00 +0200
Organization: Also freenews.netfront.net; news.tornevall.net;
 news.eternal-september.org
Message-ID: <ofcvdf$4fr$1@dont-email.me>
References: <cf1c1eb7-61cf-4ee5-8837-d4a95f95a4ba@googlegroups.com>
 <of7t2m$pdb$1@dont-email.me> <lyd1bahray.fsf@pushface.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 15 May 2017 19:26:39 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="c7c052a4c88e1c3d69d26111316a50aa";
	logging-data="4603"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/QEMgGXXA6qsYnSEMH/wpEVz8/BsNKyR8="
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.8.0
In-Reply-To: <lyd1bahray.fsf@pushface.org>
Cancel-Lock: sha1:GjG1zcDIEVGINJO/WlHdwqNTrEo=
Xref: news.eternal-september.org comp.lang.ada:46790
Date: 2017-05-15T21:30:00+02:00
List-Id: <comp.lang.ada>

On 05/15/2017 09:07 PM, Simon Wright wrote:
>
> I was thinking that an alternative subject area might be code like
>
>       procedure Add (Dest : in out Integer; N : Integer)
>         with
>           Post => Dest = Dest'Old + N;
>
>       procedure Add (Dest : in out Integer; N : Integer)
>       is
>       begin
>          Dest := Dest + N;
>       end Add;
>
>       Dest : Integer := 42;
>
>    ...
>
>       Add (Dest, Dest);
>
> (where we have alternate paths to the variable Dest); but SPARK is happy
> and the runtime check isn't triggered, so I suppose the ARM supports
> this (by copy-out?).

Elementary types are passed by copy, so you don't have any paths to the variable 
Dest inside Add. That's why this is OK. If the type might be by reference, 
though, this can be a problem.

-- 
Jeff Carter
"Strange women lying in ponds distributing swords
is no basis for a system of government."
Monty Python & the Holy Grail
66