一种用于指针程序的形状分析方法  

An Approach for Analysis of Pointer Programs

作　　者：刘刚[1] 胡凯平[1] 宋发兴[1] 

机构地区：[1]中国人民解放军63898部队

出　　处：《计算机与现代化》2012年第4期82-85,共4页Computer and Modernization

摘　　要：指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻辑进行扩展而得到的程序逻辑。首先介绍所提出的形状图和形状图逻辑;然后在此基础之上,设计一种基于形状图逻辑的形状分析方法。Analysis of pointer programs has already become a hotspot research in the field of programming languages.This paper takes an approach to the problem by doing shape analysis,which uses a shape graph to express points-to and equivalence relations among pointers in a program,and uses a shape graph logic to infer programs.The shape graph logic is an extension to Hoare logic by regarding shape graphs as assertions about pointers directly.First,this paper describes the proposed shape graph and shape graph logic.Then based on the shape graph logic,it designs a method for shape analysis on pointer programs.

关 键 词：形状图 形状图逻辑 HOARE逻辑 形状分析 程序分析 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]