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

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

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

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

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

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

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

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

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

2.選擇驗證分析模式

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

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

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

Function_sub(){ ……};

Function_top(){……

Function_sub();

……};

自動生成的main函數中只調用Function_top：在分析Function_top的進程中分析Function_sub，即Function_sub在Function_top的上下文中被分析。

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

— 總結 —

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

往期 | 代碼分析驗證

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

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