Spark, pragma

Prev: Ada compilers written in ... (was: Re: Ada noob here! Is Ada widely used?)
Next: Sockets package in SPARK

From: Alexandre K on 28 May 2010 03:34

---

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

From: Yannick Duchêne (Hibou57) on 28 May 2010 03:50

---

Le Fri, 28 May 2010 09:34:48 +0200, Alexandre K
<alexandre.nospam(a)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.

From: Alexandre K on 28 May 2010 05:08

---

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

From: Yannick Duchêne (Hibou57) on 28 May 2010 05:26

---

Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K
<alexandre.nospam(a)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.

From: Alexandre K on 28 May 2010 05:54

---

On 28 mai, 11:26, Yannick Duchêne (Hibou57) <yannick_duch...(a)yahoo.fr>
wrote:
> Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K  
> <alexandre.nos...(a)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.

 |  Next  |  Last
Pages: 1 2
Prev: Ada compilers written in ... (was: Re: Ada noob here! Is Ada widely used?)
Next: Sockets package in SPARK