From: Stuart Palin <stuart.palin@gecm.com>
Subject: Re: Idea: Array Boundary Checks on Write Access Only
Date: 1998/06/18
Date: 1998-06-18T00:00:00+00:00 [thread overview]
Message-ID: <3588DE63.A3F@gecm.com> (raw)
In-Reply-To: 3588D738.4BB32E5A@cl.cam.ac.uk
Markus Kuhn wrote:
>
> Lieven Marchand wrote:
> > About the only commonly used case that most compilers don't handle is
> > where you put in the check yourself.
>
> It would be really neat if Ada compilers would keep track not only of
> the declared range of a subtype, but also of the effectively possible
> range of Integer variables inside a certain program fragment as part
> of the flow analysis.
<snip>
The Praxis Critical Systems work with SPARK has recognised this need for
'shallow-proofs' and they have some very interesting ideas and the tool
support to back it up.
Try looking at http://www.praxis-cs.co.uk/
--
Stuart Palin
Consultant Engineer
Flight Systems Division (Rochester)
GEC-Marconi Avionics Ltd
next prev parent reply other threads:[~1998-06-18 0:00 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
1998-06-15 0:00 Idea: Array Boundary Checks on Write Access Only Markus Kuhn
1998-06-15 0:00 ` Peter Amey
1998-06-20 0:00 ` Robert Dewar
1998-06-21 0:00 ` Markus Kuhn
[not found] ` <dewar.898490510@merv>
1998-07-09 0:00 ` Frank Klemm
1998-06-17 0:00 ` Stephen Leake
1998-06-17 0:00 ` Markus Kuhn
1998-06-17 0:00 ` Robert A Duff
1998-06-18 0:00 ` Anonymous
1998-06-18 0:00 ` Stuart Palin
[not found] ` <6m8v02$r2l$1@xenon.inbe.net>
1998-06-18 0:00 ` Markus Kuhn
1998-06-18 0:00 ` Lieven Marchand
1998-06-20 0:00 ` Robert I. Eachus
1998-06-18 0:00 ` dennison
1998-06-18 0:00 ` Stuart Palin [this message]
1998-06-18 0:00 ` dennison
1998-06-20 0:00 ` Robert Dewar
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox