共用方式為


狀態窗格

[ 狀態 ] 窗格會顯示驅動程式、作業系統模型和規則中變數值的布林運算式。 SDV 使用這些運算式來建構驅動程式、作業系統模型和規則的抽象概念,並在驗證中使用它們。

下列螢幕擷取畫面顯示 [瑕疵檢視器] 中的範例 [ 狀態 ] 窗格。

[瑕疵檢視器] 中 [狀態] 窗格的螢幕擷取畫面。

[ 狀態 ] 窗格是瑕疵檢視器的元件。 在 [ 追蹤樹狀結構] 窗格中醒目提示程式碼專案,並在 [ 原始程式碼] 窗格中醒目提示對應的源程式碼時, [狀態 ] 窗格會顯示 [狀態] 窗格 (從 SDV 追蹤驅動程式的運算式集) ,在執行程式程式碼之前評估為 TRUE 的驅動程式 (。

追蹤布林運算式

驗證驅動程式的每個規則時,SDV 會追蹤一組布林運算式。 [ 狀態 ] 窗格中顯示的布林運算式是評估為 TRUE的運算式。 如果 [追蹤樹 狀結構] 窗格中的 元素變更了任何運算式的值, [狀態 ] 窗格的內容就會變更,以顯示評估為 TRUE的新運算式集。

解譯狀態窗格中的運算式

出現在 [ 狀態 ] 窗格中的大部分運算式都與規則程式碼中明顯的變數相關。 您可以在 [原始程式碼] 窗格的RuleName.slic檔案中使用規則 (原始程式碼) ,以協助您解譯運算式。

不過,有些運算式會出現在 [ 狀態 ] 窗格中,而不會有任何其內部標記法的詳細資料,可協助您解譯這些運算式。 例如

x!=x

對於 SDV,此運算式代表一個條件,在此條件中,追蹤中的變數 x 值不等於追蹤中不同點上相同變數的值。 使用驅動程式原始程式碼、規則程式碼 (*.slic) ,以及 [追蹤樹狀結構 ] 窗格中的專案,協助您解譯運算式。

狀態窗格中的步驟索引標籤

[ 狀態 ] 窗格中的布林運算式會顯示在索引標籤上。 每個索引標籤都代表在驗證中使用的所有原始程式碼追蹤中的步驟。 步驟索引標籤上的數位代表追蹤中該步驟的順序。

一般而言,因為每一行原始程式碼都只代表追蹤中的一個步驟,所以 [ 狀態 ] 窗格中只會有一個步驟索引標籤。 不過,複雜的程式碼可能會產生許多步驟。

例如,下列螢幕擷取畫面顯示 [狀態] 窗格,其中顯示包含函式指標的程式程式碼。 在此情況下,每個步驟索引標籤代表指標解析中的步驟、指向函式的呼叫及其結果。 (步驟索引標籤數目會顯示 SDV 解析函式指標所需的步驟數。)

[狀態] 窗格的螢幕擷取畫面,其中顯示具有函式指標的程式程式碼。

若要依序檢視 [ 狀態 ] 窗格中的每個步驟索引標籤,請在 [原始程式碼 ] 窗格中選取相關聯的程式程式碼。 然後,重複按一下 [原始程式碼 ] 窗格中的程式程式碼。 每次按一下選取的程式程式碼時,SDV 都會顯示下一個步驟索引標籤,直到您迴圈完成所有步驟索引標籤為止。 弧形黃色箭號表示選取的步驟。

指出所選步驟的弧形黃色箭號圖示。

您也可以按一下 [ 狀態 ] 窗格中的任何索引標籤來檢視其內容。

評論

SDV 通常會追蹤 [ 狀態 ] 窗格中未出現在規則中的運算式,而且不會與規則直接相關。 這些運算式是由 SDV 在其嘗試相互關聯不同值和不同規則違規時所使用的複雜啟發學習法所產生。 在某些情況下,SDV 無法正確評估運算式。 在這些情況下,SDV 會提供訊息,指出目前狀態不明,並顯示步驟中具有最後一個已知狀態的運算式。 如需說明,請參閱下列程式碼範例:

Unknown state. Last known state from step 120.
sdv irql current ==2
sdv irql current!=1
sdv irql current!=0