基于CEGAR的C程序空指針解引用檢測(cè).pdf

1、隨著計(jì)算機(jī)硬件技術(shù)的發(fā)展，計(jì)算機(jī)軟件系統(tǒng)的復(fù)雜性越來(lái)越高，所涉及的代碼量越來(lái)越大，同時(shí)程序中的錯(cuò)誤和問(wèn)題隱患也越來(lái)越多。因此，如何提高軟件系統(tǒng)的可靠性和安全性已成為計(jì)算機(jī)軟件領(lǐng)域的一個(gè)緊迫需求。
　　軟件模型檢測(cè)技術(shù)是提高程序可靠性和安全性的重要途徑。該技術(shù)可以自動(dòng)化地驗(yàn)證程序是否可以滿(mǎn)足一些關(guān)鍵性質(zhì)。C語(yǔ)言是目前軟件領(lǐng)域最為廣泛使用的編程語(yǔ)言之一。它的語(yǔ)法規(guī)范比較靈活，尤其是對(duì)指針的使用，稍微不注意，就會(huì)導(dǎo)致程序崩潰。在C程序中

2、，對(duì)指針的不正確使用，會(huì)帶來(lái)如內(nèi)存泄露，指針未初始化、多次釋放，以及空指針解引用等問(wèn)題。本文研究基于CEGAR技術(shù)的C程序空指針解引用的檢測(cè)算法。首先，實(shí)現(xiàn)了基于CEGAR的C程序PPTL模型檢測(cè)算法。在此基礎(chǔ)上，通過(guò)PPTL公式來(lái)描述空指針解引用的特征，進(jìn)一步檢測(cè)C程序中是否存在空指針解引用的問(wèn)題。為了提高驗(yàn)證的自動(dòng)化水平，本文通過(guò)對(duì)C源代碼進(jìn)行掃描，對(duì)所涉及到的指針自動(dòng)產(chǎn)生待驗(yàn)證的PPTL性質(zhì)，避免了手動(dòng)在C程序中加入斷言所帶來(lái)的麻