Newby-ish question -- SPARK v. Ada2005 problem

Newby-ish question -- SPARK v. Ada2005 problem

[Tim Rowe]

Looking at the tokeneer source, I find (in spark_io.adb, starting line 
123) the function:
   function File_Ref( File : File_Type) return Ada.Text_IO.File_Type
with (amongst others) the return statement:
       when NamedFile => return File.File.all;

Ada.Text_IO.File_Type is a limited type, and gnat informs me that this 
is illegal in Ada2005 because you can't copy objects of limited type 
(RM-2005 6.5(5.5/2), so there's a bit more to it). Gnat's recommended 
solution of using an access type instead is out if I want the code to be 
SPARK compliant, and (as a confessed neophyte) I can't see a way out of 
this other than hiding the code from SPARK (or using the -gnat95 
compiler flag, of course). Is there something obvious that I'm missing?

Thanks in advance!

Re: Newby-ish question -- SPARK v. Ada2005 problem

[roderick.chapman]

Basically, you're correct - Tokeneer is written in SPARK95,
so you need the -gnat95 switch to compile.  This is specified
in the code/common.gpr project file that accompanies the
release.

Someday, we'll update SPARK_IO to be compatible with Ada2005...
 - Rod Chapman, SPARK Team

Compiler Warnings while building the SPARK Tokeneer

[anon]

In compiling Sparks 8.1.1 I saw a number of style and "pragma Unreferenced"
generated warnings. I just wonder if these are the only type of warnings or
if others exist that might cause problems. And for the GNAT and SPARK 
systems, all warnings should be treated as errors. 

Plus this type of programming kind of reminds me of bad side of C/C++ 
coding.

Re: Newby-ish question -- SPARK v. Ada2005 problem

[Tim Rowe]

roderick.chapman@googlemail.com wrote:
> Basically, you're correct - Tokeneer is written in SPARK95,
> so you need the -gnat95 switch to compile.  This is specified
> in the code/common.gpr project file that accompanies the
> release.

I was wondering about my own new code -- is there a way I could have 
written that function in Ada 2005 and still be compatible with SPARK?