分享配置Polyspace分析C代碼的方法和簡介

Polyspace可以分析C、C++以及Ada代碼，本文以嵌入式系統(tǒng)中最為常見的C代碼分析為例說明Polyspace配置一個工程的過程和注意事項。

1. 配置語言和處理器類型

C語言由于其靈活性，在不同的編譯器中有不同的約束和擴展，會影響最終生成的目標碼的行為。Polyspace分析C代碼時首先要最大程度和目標編譯器的行為保持一致，這樣才能保持代碼分析的意義。因此在開始創(chuàng)建Polyspace工程時，我們需要配置編譯器和處理器類型：

所選用的C語言標準：C90/C99

所用編譯器類型：Keil/Tasking/Diab/IAR…

（編譯器通常定義了標準C語言之外的擴展，如關(guān)鍵字sfr、sbit等。選定編譯器類型相當(dāng)于告知了Polyspace在遇到此類非標擴展時如何解釋其行為。）

目標處理器類型：定義不同數(shù)據(jù)類型的大小和字節(jié)順序類型，如mpc5xx系列處理器定義如下：

（某些運行時錯誤檢查與此有關(guān)，如同一變量在Int定義為16位時會發(fā)生溢出，而在Int定義為32位時不會發(fā)生溢出。）

其他編譯器行為設(shè)定：如負除取整方向、有符號數(shù)右移邏輯、枚舉類型定義方式等。

2.選擇驗證分析模式

Polyspace有兩種基本的驗證分析模式：應(yīng)用級分析和模塊級分析，可以分別對應(yīng)于集成測試和單元測試。

所謂應(yīng)用級分析指用戶待分析的源代碼中包含了 main函數(shù)，選擇應(yīng)用級分析即分析進程從用戶main函數(shù)入口，為了更好地模擬實際程序運行和調(diào)度情形，有時需要進行多任務(wù)（Multitasking）設(shè)置，有機會在以后再進一步介紹。

模塊級分析通常待分析代碼不包含main函數(shù)，Polyspace會自動打樁生成main函數(shù)并建立待分析函數(shù)的調(diào)用關(guān)系進行分析，并可進一步根據(jù)需要細化配置。如對于以下被調(diào)函數(shù)Function_sub和主調(diào)函數(shù)Function_top，可以設(shè)置為以下兩種分析入口形式：

Function_sub(){ ……};

Function_top(){……

Function_sub();

……};

自動生成的main函數(shù)中只調(diào)用Function_top：在分析Function_top的進程中分析Function_sub，即Function_sub在Function_top的上下文中被分析。

自動生成的main函數(shù)中同時調(diào)用Function_top和Function_sub：Function_sub除了在Function_top的上下文中被分析，也會在直接在main函數(shù)上下文中被分析。對應(yīng)的可能場景是Function_sub會被其他函數(shù)調(diào)用，需要更為魯棒地分析其安全性。

— 總結(jié) —

Polyspace的配置是一個既簡單又靈活的過程，通過對編譯器行為的模擬和分析模型的選擇，我們可以得到更為有意義和更符合需要的結(jié)果。

往期 | 代碼分析驗證

Polyspace應(yīng)用到軟件開發(fā)和驗證流程

淺談Polyspace的靜態(tài)分析