Re: eliminating array bounds checking overhead

r_c_chapman@my-deja.com
1 May 2000 13:23:20 -0400

          From comp.compilers

Related articles
[11 earlier articles]
Re: eliminating array bounds checking overhead tej@melbpc.org.au (Tim Josling) (2000-04-30)
Re: eliminating array bounds checking overhead markw65@my-deja.com (Mark Williams) (2000-04-30)
Re: eliminating array bounds checking overhead d95josef@dtek.chalmers.se (2000-04-30)
Re: eliminating array bounds checking overhead mayur_naik@my-deja.com (2000-04-30)
Re: eliminating array bounds checking overhead terryg@uswest.net (Terry Greyzck) (2000-05-01)
Re: eliminating array bounds checking overhead monnier+comp/compilers/news/@flint.cs.yale.edu (Stefan Monnier) (2000-05-01)
Re: eliminating array bounds checking overhead r_c_chapman@my-deja.com (2000-05-01)
Re: eliminating array bounds checking overhead markw65@my-deja.com (Mark Williams) (2000-05-04)
Re: eliminating array bounds checking overhead world!bobduff@uunet.uu.net (Robert A Duff) (2000-05-04)
Re: eliminating array bounds checking overhead paule@martex.gen.oh.us (Paul Evans) (2000-05-04)
Re: eliminating array bounds checking overhead d95josef@dtek.chalmers.se (Josef Sveningsson) (2000-05-12)
Re: eliminating array bounds checking overhead mtimmerm@opentext.nospam-remove.com (Matt Timmermans) (2000-05-12)
| List of all articles for this month |

From: r_c_chapman@my-deja.com
Newsgroups: comp.compilers
Date: 1 May 2000 13:23:20 -0400
Organization: Deja.com - Before you buy.
References: 00-04-194
Keywords: code, performance

> 1. index an array without checking its bounds


A completely different appraoch to this problem is taken by SPARK,
which is used in safety-critical systems (e.g. EuroFighter,
Lockheed C130J)


In SPARK, we can generate verification conditions (VCs) the proof of
which show that such a run-time check can never fail. (SPARK is an
annotated subset of Ada95 for those of you who've never heard of
it... :-) )


The Examiner (SPARK's static analysis tool) can generate such VCs for
all instances of predefined exceptions. Once the proofs are
discharged, then the compiler can _justifiably_ be instructed to
simply eliminate the checking code.


  - Rod Chapman
      Praxis Critical Systems
      http://www.praxis-cs.co.uk/


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.