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!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada 2012 Constraints (WRT an Ada IR)
Date: Tue, 13 Dec 2016 17:19:30 -0600
Organization: JSA Research & Innovation
Message-ID: <o2pvm3$sa$1@franka.jacob-sparre.dk>
References: <o2f8f5$ia2$2@franka.jacob-sparre.dk>
 <eb0po8Fgob2U1@mid.individual.net> <o2ng3r$6nq$1@franka.jacob-sparre.dk>
 <ebb502F17nuU1@mid.individual.net>
NNTP-Posting-Host: rrsoftware.com
X-Trace: franka.jacob-sparre.dk 1481671171 906 24.196.82.226 (13 Dec 2016
 23:19:31 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 13 Dec 2016 23:19:31 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
X-RFC2646: Format=Flowed; Response
Xref: news.eternal-september.org comp.lang.ada:32799
Date: 2016-12-13T17:19:30-06:00
List-Id: <comp.lang.ada>

"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message 
news:ebb502F17nuU1@mid.individual.net...
...
> Yes. Also the output from CodePeer can be rather voluminous and hard to 
> understand, or so I have been told by my colleagues who are actively using 
> it. I aim to start using it, as soon as other tasks permit :-)

Exactly. That's the problem with using optimizer technology as the basis of 
correctness checking.

In my case, I have the optimizer, and I know(*) how to use it to "prove" 
preconditions/postconditions, but how to give feedback to the programmer is 
elusive. That's especially true as one mostly wants to report the negatives: 
Pre/Post that could not be eliminated by the optimizer. For obvious reasons, 
the optimizer doesn't pay much attention to things it can't do.

(*) "Know" in the sense that I have a plan which should work based on the 
existing design of the optimizer. As with all things compiler, one doesn't 
really "know" until it's implemented and tested.

Of course, instead of working on a "fun" project like this, I'm trying to 
track down why Ada.Tags is visible in a package specification that doesn't 
"with" Ada.Tags. Ada visibility and resolution sadly take all of the fun out 
of compiler construction. :-)

                                             Randy.