Path: utzoo!utgpu!attcan!uunet!lll-winken!ames!mailrus!uflorida!haven!adm!smoke!gwyn
From: gwyn@smoke.BRL.MIL (Doug Gwyn )
Newsgroups: comp.lang.c
Subject: Re: YALF (yet another lint foulup)
Message-ID: <9294@smoke.BRL.MIL>
Date: 7 Jan 89 00:41:39 GMT
References: <9255@smoke.BRL.MIL> <379@lakart.UUCP> <9341@ihlpb.ATT.COM>
Reply-To: gwyn@brl.arpa (Doug Gwyn (VLD/VMB) <gwyn>)
Organization: Ballistic Research Lab (BRL), APG, MD.
Lines: 11

In article <9341@ihlpb.ATT.COM> nevin1@ihlpb.UUCP (55528-Liber,N.J.) writes:
>Never returning is a hard property to check in C.

In fact it's impossible in general, because that would imply the
existence of a perfect decision procedure.  For example, suppose
that a proof-searching function returns if and only if it finds a
proof of Fermat's last theorem.  We don't know whether or not it
will "ever" return.  (Actually, since there are finite resources
in the run-time environment, if the algorithm cannot get into an
infinite loop then it must terminate eventually, but it may well
take longer than the age of the universe to do so.)