Re: Spark, pragma

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.