【摘要】 提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元属性设计了相应的断言演算规则和演算过程中生成验证条件的方法.该方法可以解决访问路径别名判断、指针越界访问检查、非法指针解引用检查等问题.该方法已经在一个基于演绎推理的安全C语言验证系统中实现,并且成功验证了教材上常用的一些经典算法.更多还原

【Abstract】 This paper proposes a method for verifying C programs involving operations of stack pointers name and static of area pointers.To represent pointer,the for it,which of a the method defines the triple-attribute state includes the and size the data block that the points to,as well as the offset of the pointer on the data block.By extending Hoare logic,we have designed assertion calculus pointer alias,wild for generating pointer verification conditions verification based system on the triple-attribute.programs The method is capable of detecting has path rules pointer and illegal de-reference.A for C based on deductive reasoning implemented the method and successfully implemented some classic algorithms in textbooks.更多还原