靜態驅動程式驗證器一般工具和技術限制

發行項
06/15/2023

SDV 具有下列一般限制：

SDV 一次只會驗證一個驅動程式，而且驅動程式必須遵循其中一個驅動程式模型才能完整驗證：WDM、KMDF、NDIS 或 Storport。如需支援之驅動程式的詳細資訊，請參閱判斷靜態驅動程式驗證器是否支援驅動程式或程式庫。
不屬於上述其中一個類別的驅動程式將會在可以驗證的規則中受到嚴重限制，而且在分析期間可能會失敗。
驅動程式專案檔和原始程式碼必須位於本機電腦上。您無法從遠端驗證驅動程式。
SDV 會隨英文 (美國) 地區設定一起安裝。因此，地區設定相依元素，例如字串格式設定，請使用英文 (美國) 變體。即使 SDV 安裝在英文 (美國) 以外的當地語系化 Windows 版本時，仍會出現這項限制。

SDV 驗證引擎有技術限制，可防止它正確地解譯某些驅動程式程式碼。具體來說，驗證引擎：

無法辨識 32 位整數限制為 32 位。因此，它不會偵測溢位或下溢錯誤。
請確定已正確處理使用 static 關鍵字宣告其進入點的驅動程式。不過，為了確保可辨識靜態進入點，SDV 需要變更靜態函式的 Sdv-map.h 檔案：例如，如果您宣告靜態進入點：
```
static DRIVER_UNLOAD Unload;
```
Sdv-map.h 不會包含 fun_DriverUnload的一般專案。
```
#define fun_DriverUnload Unload
```
相反地，您會看到函式名稱已管理：
```
  #define fun_DriverUnload sdv_static_function_Unload_1
```
這是必要的，因為多個模組可能會有一個名為 Unload的靜態函式。名稱會受到管理，以避免潛在的衝突。
無法解譯匯出驅動程式中定義的驅動程式分派或驅動程式回呼函式，其中匯出驅動程式具有隱藏驅動程式分派函式的模組定義 (.def) 檔案。若要避免此問題，請將驅動程式分派函式新增至 module-definition (.def) 檔案的 EXPORTS 區段。
如果這個函式的下列參考不在相同的 編譯單位中，則無法成功偵測函式的角色類型。
- 函式的宣告。
- 函式的定義。
- 將函式指派給驅動程式進入點或回呼函式。
編譯單位在此定義為最小一組原始程式碼檔案，以及此原始程式碼檔案所包含的其他原始程式檔。

如果 SDV 未偵測到函式角色類型，SDV 將不會驗證源自此函式的追蹤。

例如，如果驅動程式定義 (或實作) mydriver.c 檔案中的 EvtDriverDeviceAdd 函式。此編譯單位 (或任何 mydriver.c 包含的 .h 檔案) 必須包含 EvtDriverDeviceAdd 函式的函式角色類型宣告。
不會解譯結構化例外狀況處理。針對 try/except 語句，SDV 會分析受防護區段，就像未擲回例外狀況一樣。不會分析運算式或例外狀況處理常式程式碼。
```
// The try/except statement
__try 
{
   // guarded section
}
__except ( expression )
{
   // exception handler
} 
```
針對 try/finally 語句，SDV 會分析受防護區段，然後分析終止處理常式，就像未擲回例外狀況一樣。
```
// The try/finally statement
__try {
   // guarded section
}
__finally {
   // termination handler
}
```
針對 try/except 和 try/finally 語句，SDV 會忽略 leave 語句。

針對 try/except 和 try/finally 語句， try 區塊的跳離會防止分析 except 或 finally 語句。如需如何重寫以使用 leave 語句的相關資訊，請參閱編譯器警告 C6242的主題。
忽略指標算術。例如，它會遺漏指標遞增或遞減的情況。這項限制可能會導致誤判和誤判結果。
忽略等位。在大部分情況下，聯集會被視為結構，這可能會導致誤判或誤判。
忽略轉型作業，因此它會遺漏重新傳播所解決的兩個錯誤，以及轉換所造成的錯誤。例如，引擎假設重新轉型為字元的整數仍然具有整數值。
只初始化函式指標陣列的陣列。 SDV 發出警告，並將陣列初始化運算式壓縮為前 1000 個專案。對於其他陣列類型，只會初始化第一個專案。
不會呼叫陣列中初始化之物件的建構函式。例如，在下列程式碼片段中， x 不會設定為 10，因為 SDV 不會呼叫建構函式。
```
class A
{
public:
    A() {
      x = 10;
    }

    int x;
};

void main()
{
    A a[1];
}
```
SDV 不支援使用建構函式來初始化陣列。例如，在下列程式碼片段中，主要函式中不會正確呼叫 P 的建構函式，而且不會初始化陣列 p2 中的元素：
```
class P
{
public:
    P() : x(0) {}
    int x;
};

void main()
{
    P* p1 = new P[1];

    P p2[1] = {P()};
}
```
SDV 會忽略先行編譯的標頭。僅使用先行編譯標頭來加速編譯的驅動程式，將會使用 SDV 編譯速度較慢。必須使用先行編譯標頭進行成功編譯的驅動程式將不會使用 SDV 進行編譯。
無法推斷透過 呼叫 RtlZeroMemory 或 NdisZeroMemory進行的一些隱含指派類型。引擎會盡最大努力地將記憶體初始化為零，但只有在它可以識別其類型時。因此，相依于這些函式來初始化記憶體的程式碼可能會沿著某些程式碼路徑產生誤判。
不支援允許其追蹤 I/O 要求的手動分派至 KMDF 驅動程式的記憶體模型。引擎僅支援依賴架構將 I/O 要求傳遞給驅動程式 (的方法，以進行循序或平行分派) 。
不支援使用 float 資料類型進行比較。這項技術限制可能會產生誤判和誤判結果。
SDV 不支援虛擬繼承或虛擬函式。 SDV 不會透過虛擬函式產生遵循程式碼路徑的瑕疵，這可能會導致遺失真正的瑕疵。虛擬繼承會被視為一般繼承，這可能會導致錯誤瑕疵或遺失真正的瑕疵。

共用方式為

靜態驅動程式驗證器一般工具和技術限制

意見反應

其他資源