C編程語言的普及，以及它的許多陷阱和陷阱，導致了MISRA C在C用于高完整性軟件的領域取得了巨大的成功。這一成功促使工具供應商提出了許多MISRA C檢查器的競爭實現。工具在它們幫助執行的MISRA C指南的覆蓋范圍上尤其競爭，因為不可能執行MISRA C的所有16個指令和143個規則（統稱為指南）。

特別是，143 條規則中有 27 條是不可判定的，因此沒有工具可以始終檢測所有違反這些規則的行為，同時報告不構成違規的代碼的“誤報”。不可判定規則的一個例子是規則1.3：“不得發生未定義或關鍵的未指定行為。MISRA C：2012 的附錄 H 列出了 C 編程語言標準中數百個未定義和關鍵未指定行為的案例，其中大多數無法單獨判定。在大多數情況下，MISRA C 檢查器忽略了不可判定的規則，例如規則 1.3，盡管已知違反這些規則會對軟件質量產生巨大影響。

但是，對于其他編程語言，可以使用靜態分析技術來應對這一挑戰，而不會使用戶誤報淹沒。一個例子是由AdaCore，Altran和Inria開發的SPARK工具集，它基于四個原則：

基礎語言 Ada 通過定義明確的語言標準、強大的類型化和豐富的規范功能為靜態分析提供了堅實的基礎。

Ada 的 SPARK 子集通過控制歧義來源（如函數中的副作用和名稱的別名）以基本方式限制基本語言以支持靜態分析。

靜態分析工具主要以單個函數的粒度工作，使分析更加精確，并最大限度地減少誤報的可能性。

靜態分析工具是交互式的，允許用戶在必要時或需要時指導分析，并在用戶提供的合同無法證明時提供反例。

SPARK 可以在 C 代碼庫中逐步采用，通過SPARK 采用的五個級別以及支持將形式分析 （SPARK） 與傳統的基于測試的方法 （C） 相結合的“混合驗證”來逐步獲得保證。

火花石等級 - 基本保證

SPARK采用的第一級稱為石頭級。它對應于符合 Ada 的 SPARK 子集的代碼。僅采用此級別即可保證許多無法對 C 強制執行的一致性屬性。其中包括：

使用適當的包系統，而不是C使用基于文本的文件，沒有翻譯單元的一致性要求;

嚴格且可讀的語法，強調清晰度并最大限度地減少“陷阱”，而不是 C 非常寬松的語法，這使得編寫效果不是預期程序變得容易，

遵守 Ada 和 SPARK 的強類型規則，而不是 C 的“糟糕的類型安全性，允許發生廣泛的隱式類型轉換，這可能會損害安全性，因為它們的實現定義方面可能會導致開發人員混淆。（MISRA C：2012，附件C）

MISRA C試圖通過各種準則來馴服C語言的這些可能的不一致之處。它特別定義了更強的類型規則（“基本類型模型”），并限制函數參數/結果和控制結構的使用。雖然這些避免了開發人員混淆的常見來源，但它們故意不是防彈的，否則它們會使大多數 C 程序非法。

這些基本保證在SPARK中很容易實現，通過一個名為GNATprove的工具進行簡單的類似編譯器的分析，這要歸功于定義Ada的SPARK子集的更強大的規則。

SPARK 銀級 - 強大的安全和安保保證

MISRA-C 指南還旨在防止更細微的錯誤、未初始化數據的讀取、表達式中沖突的副作用以及未定義的行為，例如除以零或緩沖區溢出（這可能具有安全后果）。所有這些都屬于不可判定規則的范疇，很少有MISRA C檢查器提供完整的檢測。

在 SPARK 采用的銀牌級別完全可以防止這些情況，這對應于通過流分析（達到稱為銅牌的 SPARK 采用的第二級）和證明沒有運行時錯誤（達到第三級，即白銀）來分析程序。要達到此級別，開發人員通常需要定義具有特定約束的類型，這些約束旨在支持和提供文件之間導出的函數的協定 - 使用所謂的前提條件來指定調用方的義務，以及后置條件來指定被調用方的義務。

達到銀級的過程涉及與 IDE 的交互。開發人員運行 GNATprove 工具（可能在程序的子集上），調查 GNATprove 診斷，相應地更新程序，然后重復。GNATprove 在每一步都提供的詳細信息促進了這種交互，以指導開發人員。以下是 GNATprove 顯示的消息示例：

在找到可能導致溢出的加法操作后，GNATprove 給出了一個觸發問題的值的示例，這里是最大的整數值（在 SPARK 中表示為整數‘最后）。“檢查原因”清楚地解釋了加法的結果應該適合機器整數，如果 X 是加法前的最大整數值，則情況并非如此。然后，GNATprove 建議向函數 Incr 添加一個合適的前提條件可能會解決這個問題，在這里指定 X 不能是那個最大值。

超越銀級的火花

使用SPARK還有更多的好處，遠遠超出了MISRA C檢查器所能提供的。在黃金和白金級別，開發人員通過SPARK合同指定程序的屬性，然后可以使用GNATprove 來保證這些屬性將得到滿足。開發人員還可以啟用 GNATprove 警告來檢測死代碼（也是 MISRA C 追求的目標）和代碼中的不一致，使用構成 GNATprove 分析基礎的強大證明技術。

結論

從本質上講，MISRA C追求的所有目標都可以在SPARK中最好地實現，結合更強大的基礎語言（Ada）和強大的分析工具（GNATprove）。計劃使用 MISRA C 規則的開發人員可以通過在其部分應用程序中采用 SPARK 來增強安全性。

MISRA C 中的規則代表了在關鍵應用程序中提高 C 代碼可靠性的令人印象深刻的集體努力，重點是避免容易出錯的功能，而不是強制實施特定的編程風格。然而，在基本層面上，MISRA C仍然建立在一種基礎語言之上，而這種基礎語言并不是為了支持大型高保證應用程序而設計的。很難將可靠性、安全性和安全性改造到一種從一開始就沒有這些目標的語言中。

由于 C 仍將是像 Linux 內核這樣的大型程序的基礎語言，我們可以預見兩種趨勢的共存，以更好地防止 C 程序中的錯誤，MISRA C 可以發揮作用，并用更安全的語言（如 Rust 和 SPARK Ada ）替換 C 作為部分代碼。

審核編輯：郭婷