軟件開發(fā)活動(dòng)應(yīng)包括源代碼審查，以提高軟件質(zhì)量并防止或消除軟件缺陷，靜態(tài)分析工具可以自動(dòng)化該活動(dòng)的重要部分，同時(shí)降低其成本。代碼審查通常基于定義應(yīng)識(shí)別和糾正哪些違規(guī)或缺陷的編碼標(biāo)準(zhǔn)和/或檢查表進(jìn)行。

尤其是 C 語言，編碼標(biāo)準(zhǔn)的流行示例是 MISRA C 和 CERT C，它們分別提供了增強(qiáng)安全性和安全性的指南（盡管這兩個(gè)范圍之間存在一些重疊）。MISRA C 指南的制定特別關(guān)注其靜態(tài)分析的可執(zhí)行性，這反映在可以自動(dòng)實(shí)現(xiàn)的大量執(zhí)行中。

但是，有兩個(gè)不可避免的限制阻礙了全自動(dòng)執(zhí)行：

1. 在某些情況下，將靜態(tài)分析器完全執(zhí)行準(zhǔn)則所需的所有信息形式化是不切實(shí)際的或不可能的。

2. 對(duì)于某些準(zhǔn)則，即使所有信息都可用于算法，即使算法可以擴(kuò)展以清除任何特定的假陽性或假陰性。

在最新版本的 MISRA C （2012） 中，這些限制反映在指南的分類中。當(dāng)可以提供足夠的信息時(shí)，將指南歸類為規(guī)則；否則，它被歸類為指令。當(dāng)可以構(gòu)造通用算法時(shí)，將規(guī)則分類為可判定的；否則，它被歸類為不可判定。

指南有不同的優(yōu)先級(jí)和不同的范圍，但為了初步了解自動(dòng)執(zhí)行的潛在程度，159 條指南分為 16 條指令、27 條不可判定規(guī)則和 116 條可判定規(guī)則。

指令的一個(gè)示例是所有代碼都應(yīng)可追溯至文件化要求。在這種情況下，僅向靜態(tài)分析器提供整個(gè)源代碼和用于構(gòu)建應(yīng)用程序的編譯器配置是不夠的。首先，將任何重要的要求形式化是不切實(shí)際的或不可能的。

可判定規(guī)則的一個(gè)示例是不應(yīng)使用#undef。在這種情況下，可以構(gòu)造一個(gè)算法來掃描任何源代碼并報(bào)告所有出現(xiàn)和僅出現(xiàn)#undef 預(yù)處理指令的情況。

不可判定規(guī)則的一個(gè)例子是項(xiàng)目不應(yīng)包含無法訪問的代碼。你能想象一個(gè)算法可以精確識(shí)別任何項(xiàng)目中所有無法訪問的代碼實(shí)例嗎？

不可判定性可能是一個(gè)相當(dāng)不直觀的概念。軟件開發(fā)人員通常會(huì)面臨一系列需要解決的問題，從微不足道到不可能，其中可以實(shí)現(xiàn)的限制通常由熟悉的因素決定，例如缺乏信息、問題過于復(fù)雜、資源消耗急劇增加域范圍等

除了所有這些因素之外，編碼標(biāo)準(zhǔn)的自動(dòng)執(zhí)行（或任何其他自動(dòng)檢測(cè)軟件缺陷的非正式方式）涉及構(gòu)建原則上可以自我分析的算法，這會(huì)引入一個(gè)循環(huán)性，如果一個(gè)額外的基本限制會(huì)導(dǎo)致一個(gè)悖論 - undecidability - 不妨礙構(gòu)建一個(gè)健全和完整的分析儀。

審核編輯：郭婷