Abstract:

The validation of program correctness is a challenge problem in computer science. The theory of abstract interpretation provides a general framework for static analysis which can deduce programs’ dynamic property automatically. A value range analysis based on abstract interpretation can give the invariant relationship of variables at every program point, which is very important to compilation optimization and error examination. We propose an interprocedural framework that analyses the value range information of numerical programs, which can process C and Fortran programs. The C or Fortran source program is first preprocessed to an uniform representation, and then we draw the semantic equation which is equivalent to the source semantics. Finally, the iterative computation is done on this syntax equation to get the program invariant. Besides, we model some complex syntax structures such as array. The experiment indicates that our framework is very extensive and precise, and can process most problems brought by the usage of array.

Key words: static analysis;abstract interpretation;value range analysis;numeric abstract domain;array abstraction