Eliminating Redundant Range Checks in GNAT Using Symbolic Evaluation

Implementation of strongly typed language such as Ada95 requires range checks in the presence of array index expressions and assignment statements. Range checks that cannot be resolved by the compiler have to be taken care of at run-time inducing overhead both in execution-time as well as code size of the resulting executable. We propose a new method of range check elimination based on symbolic evaluation that incorporates type information provided by the underlying programming language. We are currently implementing this technique for Ada95 within GNAT, the GNU Ada Translator.