From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,8a4455177648cb9e
X-Google-Attributes: gid103376,public
From: Stuart Palin <stuart.palin@gecm.com>
Subject: Re: Idea: Array Boundary Checks on Write Access Only
Date: 1998/06/18
Message-ID: <3588DE63.A3F@gecm.com>#1/1
X-Deja-AN: 363805742
Content-Transfer-Encoding: 7bit
References: <35851B64.5BF271C4@cl.cam.ac.uk> <6m8v02$r2l$1@xenon.inbe.net>
 <3588D738.4BB32E5A@cl.cam.ac.uk>
Content-Type: text/plain; charset=us-ascii
Organization: GEC-Marconi Avionics
Mime-Version: 1.0
Newsgroups: comp.lang.ada
Date: 1998-06-18T00:00:00+00:00
List-Id: <comp.lang.ada>


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