Polyspace可以分析C、C++以及Ada代碼,本文以嵌入式系統(tǒng)中最為常見(jiàn)的C代碼分析為例說(shuō)明Polyspace配置一個(gè)工程的過(guò)程和注意事項(xiàng)。
1. 配置語(yǔ)言和處理器類(lèi)型
C語(yǔ)言由于其靈活性,在不同的編譯器中有不同的約束和擴(kuò)展,會(huì)影響最終生成的目標(biāo)碼的行為。Polyspace分析C代碼時(shí)首先要最大程度和目標(biāo)編譯器的行為保持一致,這樣才能保持代碼分析的意義。因此在開(kāi)始創(chuàng)建Polyspace工程時(shí),我們需要配置編譯器和處理器類(lèi)型:
所選用的C語(yǔ)言標(biāo)準(zhǔn):C90/C99
所用編譯器類(lèi)型:Keil/Tasking/Diab/IAR…
(編譯器通常定義了標(biāo)準(zhǔn)C語(yǔ)言之外的擴(kuò)展,如關(guān)鍵字sfr、sbit等。選定編譯器類(lèi)型相當(dāng)于告知了Polyspace在遇到此類(lèi)非標(biāo)擴(kuò)展時(shí)如何解釋其行為。)
目標(biāo)處理器類(lèi)型:定義不同數(shù)據(jù)類(lèi)型的大小和字節(jié)順序類(lèi)型,如mpc5xx系列處理器定義如下:
(某些運(yùn)行時(shí)錯(cuò)誤檢查與此有關(guān),如同一變量在Int定義為16位時(shí)會(huì)發(fā)生溢出,而在Int定義為32位時(shí)不會(huì)發(fā)生溢出。)
其他編譯器行為設(shè)定:如負(fù)除取整方向、有符號(hào)數(shù)右移邏輯、枚舉類(lèi)型定義方式等。
2.選擇驗(yàn)證分析模式
Polyspace有兩種基本的驗(yàn)證分析模式:應(yīng)用級(jí)分析和模塊級(jí)分析,可以分別對(duì)應(yīng)于集成測(cè)試和單元測(cè)試。
所謂應(yīng)用級(jí)分析指用戶待分析的源代碼中包含了 main函數(shù),選擇應(yīng)用級(jí)分析即分析進(jìn)程從用戶main函數(shù)入口,為了更好地模擬實(shí)際程序運(yùn)行和調(diào)度情形,有時(shí)需要進(jìn)行多任務(wù)(Multitasking)設(shè)置,有機(jī)會(huì)在以后再進(jìn)一步介紹。
模塊級(jí)分析通常待分析代碼不包含main函數(shù),Polyspace會(huì)自動(dòng)打樁生成main函數(shù)并建立待分析函數(shù)的調(diào)用關(guān)系進(jìn)行分析,并可進(jìn)一步根據(jù)需要細(xì)化配置。如對(duì)于以下被調(diào)函數(shù)Function_sub和主調(diào)函數(shù)Function_top,可以設(shè)置為以下兩種分析入口形式:
Function_sub(){ ……};
Function_top(){……
Function_sub();
……};
自動(dòng)生成的main函數(shù)中只調(diào)用Function_top:在分析Function_top的進(jìn)程中分析Function_sub,即Function_sub在Function_top的上下文中被分析。
自動(dòng)生成的main函數(shù)中同時(shí)調(diào)用Function_top和Function_sub:Function_sub除了在Function_top的上下文中被分析,也會(huì)在直接在main函數(shù)上下文中被分析。對(duì)應(yīng)的可能場(chǎng)景是Function_sub會(huì)被其他函數(shù)調(diào)用,需要更為魯棒地分析其安全性。
— 總結(jié) —
Polyspace的配置是一個(gè)既簡(jiǎn)單又靈活的過(guò)程,通過(guò)對(duì)編譯器行為的模擬和分析模型的選擇,我們可以得到更為有意義和更符合需要的結(jié)果。
往期 | 代碼分析驗(yàn)證
Polyspace應(yīng)用到軟件開(kāi)發(fā)和驗(yàn)證流程
淺談Polyspace的靜態(tài)分析
-
處理器
+關(guān)注
關(guān)注
68文章
19275瀏覽量
229744 -
編譯器
+關(guān)注
關(guān)注
1文章
1634瀏覽量
49119 -
C代碼
+關(guān)注
關(guān)注
1文章
89瀏覽量
14300
發(fā)布評(píng)論請(qǐng)先 登錄
相關(guān)推薦
評(píng)論