Abstract
The incorrect use of pointers is one of the most common source of bugs. As a consequence, any kind of static code checking capable of detecting potential bugs at compile time is welcome. This paper presents a static analysis for the detection of incorrect accesses to memory (dereferences of invalid pointers). A pointer may be invalid because it has not been initialised or because it refers to a memory location which has been deallocated. The analyser is derived from an axiomatisation of alias and connectivity properties which is shown to be sound with respect to the natural semantics of the language. It deals with dynamically allocated data structures and it is accurate enough to handle circular structures.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Aho, R. Sethi and J. D. Ullman, Compilers: Principles, Techniques and Tools, Addison-Wesley publishing company, 1988.
R. Altucher and W. Landi, An extended form of must-alias analysis for dynamic allocation, in 22nd Annual ACM Symp. on Principles of Programming Languages POPL'95, Jan. 1995, pp.74–85.
L. Andersen, Program analysis and specialisation for the C programming language, Ph.D Thesis, DIKU, University of Copenhagen, May 1994.
J.-P. Banâtre, C. Bryce, D. Le Métayer, Compile-time detection of information flow in sequential programs, proc. European Symposium on Research in Computer Security, Springer Verlag, LNCS 875, pp. 55–74.
J.F. Bergeretti and B. Carré, Information-flow and data-flow analysis of while-programs, in ACM Transactions on Programming Languages and Systems,Vol. 7, No. 1, Jan. 85, pp. 37–61.
A. Bijlsma, Calculating with pointers, in Science of Computer Programming 12 (1989) 191–205, North-Holland.
R. Cartwright and D. Oppen, The logic of aliasing, in Acta Informatica 15, 365–384, 1981 ACM TOPLAS, Vol. 7, 1985, pp. 299–310.
P. Cousot and R. Cousot, Systematic design of program analysis frameworks, in 6th Annual ACM Symp. on Principles of Programming Languages POPL'79, Jan. 79, pp. 269–282.
A. Deutsch, A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations, in Proc. of the IEEE 1992 Conf. on Computer Languages, Apr. 92, pp. 2–13.
A. Deutsch, Interprocedural may-alias analysis for pointers: Beyond k-limiting, in SIGPLAN'94 Conf. on Programming Language Design and Implementation PLDI'94, Jun. 1994, pp. 230–241.
M. Emami, R. Ghiya and L. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, in SIGPLAN'94 Conf. on Programming Language Design and Implementation PLDI'94, Jun. 1994, pp. 242–256.
D. Evans, Using specifications to check source code, in Technical Report, MIT Lab for computer science, Jun. 1994.
P. Fradet, R. Gaugne and D. Le Métayer, An inference algorithm for the static verification of pointer manipulation, IRISA Research Report 980, 1996.
J. Field, G. Ramalingam and F. Tip, Parametric program slicing, in 22th Annual ACM Symp. on Principles of Programming Languages POPL'95, Jan. 95, pp. 379–392.
L. Fosdick and L. Osterweil, Data flow analysis in software reliability, ACM Computing surveys, 8(3), Sept. 1976.
C. L. Hankin, D. Le Métayer, Deriving algorithms from type inference systems: Application to strictness analysis, proc. ACM Symposium on Principles of Programming Languages, 1994, pp. 202–212, Jan. 1994.
L. Hendren and A. Nicolau, Parallelizing programs with recursive data structures, in IEEE Transactions on Parallel and Distributed Systems, Jan. 90, Vol. 1(1), pp. 35–47.
D. Jackson, Aspect: an economical bug-detector, in Proceedings of 13th International Conference on Software Engineering, May 1994, pp. 13–22.
S. Johnson, Lint, a C program checker, Computer Science technical report, Bell Laboratories, Murray Hill, NH, July 1978.
D. Luckham and N. Suzuki, Verification of array, record, and pointer operations in Pascal, in ACM Transactions on Programming Languages and Systems, Vol. 1, No.2, Oct. 1979, pp. 226–244.
J. Morris, A general axiom of assignment and Assignment and linked data structures, in Theoretical Foundations of Programming Methodology, M. Broy and G. Schmidt (eds), pp. 25–41, 1982.
S. Sagiv, N. Francez, M. Rodeh and R. Wilhelm, A logic-based approach to data flow analysis problems, in Programming Language Implementation and Logic Programming PLILP'90, LNCS 456, pp. 277–292, 1990.
R. Strom and D. Yellin, Extending typestate checking using conditional liveness analysis, in IEEE Transactions on Software Engineering, Vol. 19, No 5, May. 93, pp. 478–485.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fradet, P., Gaugne, R., Le Métayer, D. (1996). Static detection of pointer errors: An axiomatisation and a checking algorithm. In: Nielson, H.R. (eds) Programming Languages and Systems — ESOP '96. ESOP 1996. Lecture Notes in Computer Science, vol 1058. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61055-3_33
Download citation
DOI: https://doi.org/10.1007/3-540-61055-3_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61055-7
Online ISBN: 978-3-540-49942-8
eBook Packages: Springer Book Archive