* 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