Since the birth of abstract interpretation, many languages have been studied, and frameworks for their abstract interpretation have been proposed. The first languages considered by the Cousots were very simple, procedureless, FORTRAN-like languages, and were used to set up the theory. The main characteristic of this class of languages is that there is a one to one correspondence between identifiers and locations. A store can therefore be represented as a vector of a space of finite dimension. Approximating a set of memory states at a given control point thus consists in finding an abstraction (i.e. a machine-representable lattice) of this vectorial space. New problems arise however when considering a language such as Pascal, which has nested procedures, call-by-reference and recursivity, for there can be many activations of the same procedure in the run-time stack, each activation having its own environment binding identifiers to different locations anywhere in the stack by means of the call-by-address parameter passing method. The problem is therefore not only to approximate the set of values of a fixed vector of variables, but to approximate sets of run-time stacks, each stack having its own aliasing structure and being of arbitrary height. The aim of this paper is to study Pascal-like languages, and to show that it is possible to design and prove abstract interpretations used to determine assertions about scalar variables, as was formerly done for simpler languages. We shall then talk about the implementation of a specific ``semantic analyzer'' of Pascal used to determine the value range of integer variables and give some examples of the results given by this analyser.
[PostScript, PDF, © 1990 Springer-Verlag]