Spark, pragma

Spark, pragma

[Alexandre K]

Hi,
I am having trouble with Spark and pragma. If I am not wrong, Spark
accepts all pragmas and generate warning when we run the examiner. In
order than the examiner succeeds, we can tell in the warning control
file that we want to accept some or all pragma, with "pragma all".
Basically, I added a pragma Style_Checks ("-s", Off) in the beginning
of the package body.
When I run the examiner without warning control, it results a warning
about this pragma and another as a consequence :

Warning 430 - SLI generation abandoned owing to syntax or semantic
errors or multiple units in a single source file.

If run the examiner with the warning control, the warning message is
resumed, but the warning

Warning 430 - SLI generation abandoned owing to syntax or semantic
errors or multiple units in a single source file.

still exists and there is no other warning or error.
I can't understand why.

Any idea ?
Thanks

Re: Spark, pragma

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 09:34:48 +0200, Alexandre K  
<alexandre.nospam@gmail.com> a écrit:

> Hi,
> I am having trouble with Spark and pragma. If I am not wrong, Spark
> accepts all pragmas and generate warning when we run the examiner. In
> order than the examiner succeeds, we can tell in the warning control
> file that we want to accept some or all pragma, with "pragma all".
> Basically, I added a pragma Style_Checks ("-s", Off) in the beginning
> of the package body.
> When I run the examiner without warning control, it results a warning
> about this pragma and another as a consequence :
>
> Warning 430 - SLI generation abandoned owing to syntax or semantic
> errors or multiple units in a single source file.
>
> If run the examiner with the warning control, the warning message is
> resumed, but the warning
>
> Warning 430 - SLI generation abandoned owing to syntax or semantic
> errors or multiple units in a single source file.
>
> still exists and there is no other warning or error.
> I can't understand why.
>
> Any idea ?
> Thanks

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.

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

Another mention required: SPARK GPL or SPARK Pro ? They may not be the  
same... (I only have SPARK GPL in hands)

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.

Re: Spark, pragma

[Alexandre K]

> 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.

Re: Spark, pragma

[Yannick Duchêne (Hibou57)]

Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K  
<alexandre.nospam@gmail.com> a écrit:
> 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.
Ok, that is why: I have SPARK GPL 8.1.1 only.

Well, the "s" style checks stands for requirement to have a separate  
declaration for all subprograms. This is unlikely to cause a trouble with  
SPARK, even if your version was able to make special handling of these  
pragmas.

Instead, I was thinking again at your OP:

> Warning 430 - SLI generation abandoned owing to syntax or semantic
> errors or multiple units in a single source file.

It talks among other things, about a syntax error. It seems the syntax of  
this pragma is a literal, which is a letter, followed by an option On of  
Off. Here, you have "-s". Shouldn't this be "s" instead ?

May be worth to try.

-- 
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.

Re: Spark, pragma

[Alexandre K]

On 28 mai, 11:26, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K  
> <alexandre.nos...@gmail.com> a écrit:> 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.
>
> Ok, that is why: I have SPARK GPL 8.1.1 only.
>
> Well, the "s" style checks stands for requirement to have a separate  
> declaration for all subprograms. This is unlikely to cause a trouble with  
> SPARK, even if your version was able to make special handling of these  
> pragmas.
>
> Instead, I was thinking again at your OP:
>
> > Warning 430 - SLI generation abandoned owing to syntax or semantic
> > errors or multiple units in a single source file.
>
> It talks among other things, about a syntax error. It seems the syntax of  
> this pragma is a literal, which is a letter, followed by an option On of  
> Off. Here, you have "-s". Shouldn't this be "s" instead ?
>

I don't think so. I realized that in my first message I have written
"pragma Style_Checks ("s", Off)" which is incorrect in Ada.
I would want to turn off the declaration for function used just in
body.
So yes I have to use "-s", "s" would let it on because of options used
in compilation command line that make all style, warning etc as an
error.

It clearly works in Ada, it's just the examiner that reports this
error. And if I comment the pragma, the examiner succeeds.

Thanks for your advices.

> May be worth to try.
>
> --
> 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.

Re: Spark, pragma

[Alexandre K]

Well, I have got the answer. Thanks to Rod.
The SLI file is generated by the exminer since version 9.0 and is used
by GPS.

Putting a pragma before the package body results in an error because
the file not contains
1 compilation unit, but 2.
The wayround is to put the pragma inside the package body
package body P is
 pragma ...

Alex