From: moy@adacore.com
Subject: Re: Weird Bug in Get_Line
Date: Sun, 14 May 2017 14:49:06 -0700 (PDT)
Date: 2017-05-14T14:49:06-07:00 [thread overview]
Message-ID: <395b3279-cd8e-4707-8fcc-b9c4f7ee0eff@googlegroups.com> (raw)
In-Reply-To: <odr0km$tc1$1@dont-email.me>
On Wednesday, April 26, 2017 at 10:44:07 PM UTC+2, Jeffrey R. Carter wrote:
> What you've found is, as Wright pointed out, an error in GNAT's attempt to
> handle foreign files reasonably that has already been corrected, at least in the
> Pro version.
It has been fixed in early 2016 for the Pro version, and the fix was included in GNAT GPL 2016 issued last year. So 10 years later than the release date of GNAT 5.04 on which Brian reported the issue!
> TBH, handling last lines without a line terminator as if they had a line
> terminator is not easy. Much thought was needed to get PragmARC.Text_IO, which
> handles Mac (CR), Unix (LF), and Windows (CR-LF) line terminators, to do it.
The sublety of the code was the reason we went through formal verification, to make sure there were no more bugs in our implementation of Get_Line. And there were some. See the blog post Simon mentioned: http://blog.adacore.com/formal-verification-of-legacy-code
prev parent reply other threads:[~2017-05-14 21:49 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-04-26 7:38 Weird Bug in Get_Line Brian Kolden
2017-04-26 8:28 ` Brian Drummond
2017-04-26 8:42 ` Brian Kolden
2017-04-26 9:10 ` Brian Kolden
2017-04-26 10:58 ` Simon Wright
2017-04-26 17:03 ` Jeffrey R. Carter
2017-04-26 19:32 ` Brian Kolden
2017-04-26 20:44 ` Jeffrey R. Carter
2017-05-14 21:49 ` moy [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox