一种基于栈区内存模型的C程序别名判断算法

摘要 C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型的表达式,包括取地址、多级解引用、指针关系运算、结构体和数组等.基于上述内存模型,本文提出了一种判断别名的算法,使得验证工具在使用Hoare逻辑的赋值公理之前可以准确的消除断言中的别名.目前该模型已经在一个名为Safe-C验证器的程序验证工具中实现,并且成功验证了多例经典程序