* Newby-ish question -- SPARK v. Ada2005 problem
@ 2009-06-04 23:35 Tim Rowe
2009-06-05 7:36 ` roderick.chapman
0 siblings, 1 reply; 4+ messages in thread
From: Tim Rowe @ 2009-06-04 23:35 UTC (permalink / raw)
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!
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Newby-ish question -- SPARK v. Ada2005 problem
2009-06-04 23:35 Newby-ish question -- SPARK v. Ada2005 problem Tim Rowe
@ 2009-06-05 7:36 ` roderick.chapman
2009-06-05 13:32 ` Compiler Warnings while building the SPARK Tokeneer anon
2009-06-05 20:37 ` Newby-ish question -- SPARK v. Ada2005 problem Tim Rowe
0 siblings, 2 replies; 4+ messages in thread
From: roderick.chapman @ 2009-06-05 7:36 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Compiler Warnings while building the SPARK Tokeneer
2009-06-05 7:36 ` roderick.chapman
@ 2009-06-05 13:32 ` anon
2009-06-05 20:37 ` Newby-ish question -- SPARK v. Ada2005 problem Tim Rowe
1 sibling, 0 replies; 4+ messages in thread
From: anon @ 2009-06-05 13:32 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Newby-ish question -- SPARK v. Ada2005 problem
2009-06-05 7:36 ` roderick.chapman
2009-06-05 13:32 ` Compiler Warnings while building the SPARK Tokeneer anon
@ 2009-06-05 20:37 ` Tim Rowe
1 sibling, 0 replies; 4+ messages in thread
From: Tim Rowe @ 2009-06-05 20:37 UTC (permalink / raw)
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?
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2009-06-05 20:37 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-06-04 23:35 Newby-ish question -- SPARK v. Ada2005 problem Tim Rowe
2009-06-05 7:36 ` roderick.chapman
2009-06-05 13:32 ` Compiler Warnings while building the SPARK Tokeneer anon
2009-06-05 20:37 ` Newby-ish question -- SPARK v. Ada2005 problem Tim Rowe
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox