This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: [PATCH] C undefined behavior fix
- From: Rod Chapman <rod dot chapman at praxis-cs dot co dot uk>
- To: "'gcc at gcc dot gnu dot org'" <gcc at gcc dot gnu dot org>
- Date: Wed, 9 Jan 2002 12:37:49 -0000
- Subject: Re: [PATCH] C undefined behavior fix
Mike Stump wrote:
>One cure, is a completely formal language. Do you know of any real
>languages that are? By real, I mean a real language that is used to
>code real programs and used in the real world. I don't.
A language closely fitting that description is SPARK. Aside
from the details of floating point math, a full formal semantics
for SPARK were constructed a couple of years ago. These are
even freely available now on the web for the programming-language
masochists out there.
There are several projects building over 100kloc systems in SPARK now.
Most are safety-, security- or mission-critical.
The excutable core of SPARK just happens to be a strict subset of Ada,
so GNAT compiles it very well indeed, especially in its "no runtime" mode.
- Rod Chapman, Praxis Critical Systems
**********************************************************************
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.
This footnote also confirms that this email message has been swept
for the presence of computer viruses.
www.praxis-cs.co.uk
**********************************************************************