计算机工程与科学2011,Vol.33Issue(3):94-102,9.DOI:10.3969/j.issn.1007-130X.2011.03.018
一个面向C和Fortran数值程序的静态分析工具
A Static Analyzer for Numerical Programs in C and Fortran
摘要
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分类
信息技术与安全科学引用本文复制引用
侯苏宁,陈立前,王昭飞,王戟..一个面向C和Fortran数值程序的静态分析工具[J].计算机工程与科学,2011,33(3):94-102,9.基金项目
国家自然科学基金资助项目(90818024,60803042) (90818024,60803042)