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!mx02.eternal-september.org!feeder.eternal-september.org!gegeweb.org!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: Jacob Sparre Andersen <sparre@nbi.dk>
Newsgroups: comp.lang.ada
Subject: Re: {Pre,Post}conditions and side effects
Date: Tue, 19 May 2015 09:46:07 +0200
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <87617povr4.fsf@adaheads.sparre-andersen.dk>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
	<AnYlw.957256$Rp.242412@fx23.iad>
	<0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com>
	<wccoaqucn51.fsf@shell01.TheWorld.com>
	<9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com>
	<alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
	<wccegrpq2om.fsf@shell01.TheWorld.com>
	<87tww5296f.fsf@adaheads.sparre-andersen.dk>
	<871tj9dp5b.fsf@theworld.com>
	<ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
	<midvq5$2u3$1@loke.gir.dk>
	<alpine.DEB.2.11.1505071103310.14859@debian>
	<migc9a$jp8$1@loke.gir.dk>
	<alpine.DEB.2.11.1505072052570.16448@debian>
	<mijen0$1hj$1@loke.gir.dk>
	<alpine.DEB.2.11.1505111113020.12062@debian>
	<mirjho$lqh$1@loke.gir.dk>
	<alpine.DEB.2.11.1505120951500.17718@debian>
	<alpine.DEB.2.11.1505121319240.25376@debian>
	<87oali5i6n.fsf@adaheads.sparre-andersen.dk>
	<alpine.DEB.2.11.1505181348570.4352@debian>
NNTP-Posting-Host: 195.249.206.131
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: loke.gir.dk 1432021567 8202 195.249.206.131 (19 May 2015 07:46:07
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 19 May 2015 07:46:07 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)
Cancel-Lock: sha1:02/FQgo8CBhO4/FulzXFBWfu/t8=
Xref: news.eternal-september.org comp.lang.ada:25916
Date: 2015-05-19T09:46:07+02:00
List-Id: <comp.lang.ada>

Stefan.Lucks@uni-weimar.de writes:
> On Mon, 18 May 2015, Jacob Sparre Andersen wrote:

> Well, as a very simmple example, consider this:
>
> 	(for all I in 2 .. N-1 => (N mod I) /= 0)
>
> You don't need a profiler to figure out that this is prohibitively
> slow for largish N, do you?

I don't need a profiler to estimate that it takes long time to execute,
but I need a profiler to see where the compiler can't eliminate it from
a critical path through static analysis.

>> I am aware that we currently don't have as fine-grained control of
>> assertions as that would require to work well, but I assume that this
>> is something that can be discussed with the ARG and the compiler
>> vendors.
>
> This is precisely my point!

Good.  I noticed an interesting proposal for an extension to the
assertion policy control in one of the posts in this thread.  I suppose
we should push to have the ARG accept this (or something similar).

Greetings,

Jacob
-- 
There really was only one way to make a person unlearn something ...