论文部分内容阅读
本文研究了基于契约的安全分析方法。该方法通过对过程内的变量构造变量契约、对跨过程的函数调用构造函数契约描述程序的状态，并按函数调用关系自下而上获取相应的契约信息。在获取契约的基础上，使用相应的安全判定规则和更新算法实现程序安全分析。
结合C/C++语言的特点，设计和实现了针对C/C++程序安全分析的契约分析方法框架。根据C/C++安全分析实际需求，给出了C/C++指针变量前后置条件的描述方法。同时结合契约分析原理，设计了指针变量契约的数据结构，并提供一组算法，用于更新指针变量契约和对指针变量进行安全判定。
该框架具有一定的可扩展性，按需求继承相应的接口并实现对应的算法便可以使契约分析方法支持对更多C/C++类型变量的分析。