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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,cb90b009d6b31cab
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,CP1252
Path: 
 g2news2.google.com!postnews.google.com!c13g2000vbr.googlegroups.com!not-for-mail
From: Alexandre K <alexandre.nospam@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Spark, pragma
Date: Fri, 28 May 2010 02:08:37 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <9df19165-c809-48e5-b14b-b69f8af64e87@c13g2000vbr.googlegroups.com>
References: 
 <7987b9a7-b5ad-4e09-af7e-92734e551c48@f13g2000vbm.googlegroups.com>
	<op.vden1ph0ule2fv@garhos>
NNTP-Posting-Host: 82.229.198.39
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1275037717 20144 127.0.0.1 (28 May 2010 09:08:37
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 28 May 2010 09:08:37 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: c13g2000vbr.googlegroups.com; posting-host=82.229.198.39;
	posting-account=TcezFQoAAAAjIIx-1YP3Hv74ICh_b8qk
User-Agent: G2/1.0
X-HTTP-UserAgent: Opera/9.80 (Macintosh; Intel Mac OS X; U; fr) Presto/2.2.15
	Version/10.10,gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12112
Date: 2010-05-28T02:08:37-07:00
List-Id: <comp.lang.ada>

> Hi Alex,
>
> I've just tried the same as you did, a =93pragma Style_Checks ("-s", Off)=
;=94 =A0
> at the start of a package body, and could only get the classic warning, =
=A0
> not the one about SLI generation. Additionally, I could not find any =A0
> reference to a Warning 430 in the Examiner_UM documentation. Warning code=
s =A0
> exposed there stop at Warning 420, no code beyond.

But it exists in my manual, just after warning 420, and this is the
last one. (for me page 91)
Maybe as you mentionned this is due to Spark version, as I am using
Spark PRO v 9.0 with ada 2005 option.

> If this is not private stuff, can you post your body file here ?

It is not the real package, but I was experimenting few things on a
simple example, which has the error too.

 Spec:
package Test is
	type A is private;
	--# function V (I : A) return Boolean;
	function C (I : A) return Boolean;
	--  # return V (I);
	procedure Make_A (I : out A);
	--# derives I from ;
private
   subtype R is Integer range 0 .. 10;
   type A is record
      Z : R;
   end record;

end Test;

Body :
pragma Style_Checks ("-s");
package body Test is
   type E is record
      I : Integer;
   end record;
   type D is record
      J : Integer;
   end record;

   function C (I : A) return Boolean
   --# return I.Z > 10;
   is
   begin
      return I.Z > 10;
   end C;

   procedure Make_A (I : out A) is
   begin
      I :=3D A'(Z =3D> 3);
   end Make_A;
end Test;



>
> Cheers
>
> --
> There is even better than a pragma Assert: a SPARK --# check.
> --# check C and WhoKnowWhat and YouKnowWho;
> --# assert Ada;
> -- =A0i.e. forget about previous premises which leads to conclusion
> -- =A0and start with new conclusion as premise.