ABSTRACT
An approach to the elimination of run-time checks in Ada 9X is presented. The approach is a flow analysis approach based on a combination of range propagation and assertion propagation. Range propagation computes estimates for the dynamic characteristics of program entities, for example the values of objects, while assertion propagation maintains valid assertions derived from assignments and conditions of the program. This approach offers a simple alternative to the more complex approach of a theorem prover.
- 1.W. H. Harrison: Compiler Analysis of the Value Ranges for Variables. IEEE Transactions on Software Engineering, vol. SE-3, no. 3, May 1977, 243- 25OGoogle ScholarDigital Library
- 2.P. L. Mzller: Elimination of Redundant Run Time Checks in Ada 9X. master thesis, Technical Univ. of Denmark, Feb. 1993Google Scholar
- 3.A. Sakharov: Propagation of Constants and Assettions, ACM Sigplan Notices, vol. 29, no. 5, May 1994 Google ScholarDigital Library
- 4.B. Schwartz, W. Kirchg'~ssner, R. Landwehr: An Optimizer for Ada N Design, Experiences and Resuits. Proceedings of the SIGPLAN '88 Conference on Programming Language Design and Implementation, Atlanta, Georgia, June 1988, 175-184 Google ScholarDigital Library
- 5.J. Welsh: Economic Range Checks in Pascal. Software- Practice and Experience, vol. 8 (1978), 85- 97Google ScholarCross Ref
Index Terms
Run-time check elimination for Ada 9X
Recommendations
Experiences with the design of a run-time check
SAFECOMP'06: Proceedings of the 25th international conference on Computer Safety, Reliability, and SecurityRun-time checks are often assumed to be a cost-effective way of improving the dependability of software components, by checking required properties of their outputs and flagging an output as incorrect if it fails the check. Run-time checks' main point ...
Speculative improvements to verifiable bounds check elimination
PPPJ '08: Proceedings of the 6th international symposium on Principles and practice of programming in JavaAs a safety measure, the Java programming language requires bounds checking of array accesses. This usually translates to dynamic checks each time an array element is accessed. Static analysis can help eliminate some of those checks by proving them to ...
Safe, multiphase bounds check elimination in Java
As part of its type-safety regime, Java's semantics require precise exceptions at runtime when programs attempt out-of-bound array accesses. This paper describes a Java implementation that utilizes a multiphase approach to identifying safe array ...
Comments