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 X-Received: by 2002:a37:a78c:: with SMTP id q134mr7692713qke.258.1585224269041; Thu, 26 Mar 2020 05:04:29 -0700 (PDT) X-Received: by 2002:a05:6830:1513:: with SMTP id k19mr5537268otp.276.1585224268584; Thu, 26 Mar 2020 05:04:28 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 26 Mar 2020 05:04:28 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: google-groups.googlegroups.com; posting-host=76.77.182.20; posting-account=W2gdXQoAAADxIuhBWhPFjUps3wUp4RhQ NNTP-Posting-Host: 76.77.182.20 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: How do I resolve SPARK warning "procedure [...] has no effect for output procedure From: Stephen Leake Injection-Date: Thu, 26 Mar 2020 12:04:29 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader01.eternal-september.org comp.lang.ada:58251 Date: 2020-03-26T05:04:28-07:00 List-Id: On Wednesday, March 25, 2020 at 1:48:44 PM UTC-7, digitig wrote: > I'm trying to learn SPARK Ada, and, among other things, I have a procedur= e that simply puts a standard message to the screen. SPARK gives me a warni= ng that the subprogram has no effect; I can see why - it only has the side-= effect of printing to the screen. Everything I can see online to deal with = this is a) *very* old, and b) uses SPARK_Io, which I understand is obsolete= (and which I can't find). So what is the best way to tell SPARK that the p= rocedure just has that side effect? (Hopefully better than `SPARK_mode =3D>= Off'). As far as SPARK is concerned, this procedure has no effect, so analyzing it= is a waste of time. So you _should_ set SPARK_mode =3D> Off for it; that i= s the right thing to do. Why do you not want to do that? -- Stephe