Re: Spark, pragma

[Alexandre K <alexandre.nospam@gmail.com>]

> Hi Alex,
>
> I've just tried the same as you did, a “pragma Style_Checks ("-s", Off);”  
> at the start of a package body, and could only get the classic warning,  
> not the one about SLI generation. Additionally, I could not find any  
> reference to a Warning 430 in the Examiner_UM documentation. Warning codes  
> 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 := A'(Z => 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;
> --  i.e. forget about previous premises which leads to conclusion
> --  and start with new conclusion as premise.