SPARK GPL 2012 and generic, any hint?

SPARK GPL 2012 and generic, any hint?

[hugues]

Hi,

I tried SPARK GPL 2012 with a small example for generic, but I keep getting 
syntax error, do I miss something obvious?

The documentation lacks a complete example that can be processed, all I could 
find was limited code snippet :(

Here is the code source (code taken from SPARK GPL 2012 documentation, i
I simply added package stuff around)

package Test is

   generic
      type T1 is range <>;
      type T2 is range <>;
      --# check T1’Last * T1’Last <= T2’Last and
      --#       T1’First * T1’First <= T2’Last and
      --#       T1’First * T1’First >= T2’First;
   function Square (X : T1) return T2;
   --# return R => R = T2 (X * X);

end Test;

and the result for the Examiner

                              Examiner GPL 2012
             Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.
           *******************************************************


                        DATE : 08-JUL-2012 12:22:29.76


   3     generic
         ^
***        Syntax Error      : reserved word "IS" cannot be followed by 
           reserved word "GENERIC" here.

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


If I take a generic package (e.g. a stack), then I get 

---        Warning           :415: The analysis of generic packages is not yet 
           supported. It will be supported in a future release of the Examiner.

           Generating listing file stack.lst ...

which is expected from the release note.

Thankss

Re: SPARK GPL 2012 and generic, any hint?

[Phil Thornley]

In article <slrnjvinh6.n7f.hugues@soekris-1.pinkyoogx.org>, 
hugues@soekris-1.pinkyoogx.org says...
> 
> Hi,
> 
> I tried SPARK GPL 2012 with a small example for generic, but I keep getting 
> syntax error, do I miss something obvious?
> 
> The documentation lacks a complete example that can be processed, all I could 
> find was limited code snippet :(
> 
> Here is the code source (code taken from SPARK GPL 2012 documentation, i
> I simply added package stuff around)
> 
> package Test is
> 
>    generic
>       type T1 is range <>;
>       type T2 is range <>;
>       --# check T1'Last * T1'Last <= T2'Last and
>       --#       T1'First * T1'First <= T2'Last and
>       --#       T1'First * T1'First >= T2'First;
>    function Square (X : T1) return T2;
>    --# return R => R = T2 (X * X);
> 
> end Test;
> 

The instantion check isn't supported yet, and the subprogram must be at 
library level.

The following code examines OK:

   generic
      type T1 is range <>;
      type T2 is range <>;
   function Square (X : T1) return T2;
   --# return R => R = T2 (X * X);

Cheers,

Phil

Re: SPARK GPL 2012 and generic, any hint?

[hugues]

On 2012-07-08, Phil Thornley <phil.jpthornley@gmail.com> wrote:

> The instantion check isn't supported yet, and the subprogram must be at 
> library level.
>
> The following code examines OK:

Thanks, that makes sense to me now. I seldom use library-level subprograms,  
hence my miss

Regards,