Použití sestavy ověření statického ovladače

Sestava SDV je interaktivní zobrazení výsledků ověření. Tato část vysvětluje, jak vyhledat chybu kódování v ovladači pomocí sestavy SDV. Podrobné informace o sestavě, funkcích oken a prvech v oknech naleznete v tématu Sestava ověření statického ovladače.

Otevřete prohlížeč defektů statického ovladače

Pokud SDV v podokně Výsledky nahlásil nějaké "vady" (porušení předpisů), okno Prohlížeče vad v sestavě ověření statického ovladače vám umožní zobrazit část kódu, který se týká porušení. Okno Defect Viewer zobrazí kód v cestě k porušení pravidla. Pro každé pravidlo, které bylo porušeno, existuje jedno okno Prohlížeče vad (najednou můžete zobrazit pouze jedno okno Prohlížeče vad ).

Otevření okna Defect Vieweru pro vadu:

• V seznamu pod uzlem Defect(s) vyberte pravidlo.

Tento postup funguje pouze pro vady. SDV nevygeneruje okno Prohlížeče vad , pokud výsledky ověření nejsou vadami, jako jsou průchody, vypršení časového limitu, mezery, nepoužitelné nebo jakýkoli jiný výsledek, který není vadný.

Následující snímek obrazovky ukazuje stránku Zpráva ověřovače statických ovladačů.

Kontrola pravidla

Než se pokusíte najít porušení pravidla v kódu, seznamte se s pravidly, která ovladač porušil.

Část Pravidla ověření statického ovladače obsahuje téma, které vysvětluje každé pravidlo, například CancelSpinLock.

Pokud chcete zobrazit kód pravidla, klikněte v podokně Zdrojový kód sestavy statického ověření ovladače na kartu, která obsahuje kód pravidla, například CancelSpinLock.slic.

Pravidlo CancelSpinLock je například porušeno, pokud ovladač volá IoAcquireCancelSpinLock nebo IoReleaseCancelSpinLock mimo pořadí, nebo pokud ovladač ukončí rutinu před uvolněním zámku spinu.

Trasování cesty vad

Když se otevře okno Defect Viewer , vybere se prvek v podokně Trace Tree představující první volání kritického ovladače v cestě vad. V podokně Zdrojový kód je přidružený řádek zdrojového kódu zvýrazněn modře.

Následující snímek obrazovky ukazuje úvodní pohled okna Static Driver Verifier Defect Viewer pro porušení pravidla CancelSpinLock vzorkovým ovladačem Fail_Driver1. V tomto příkladu je prvním voláním v cestě k porušení pravidla CancelSpinLock volání ovladače IoAcquireCancelSpinLock v jeho rutině DispatchSystemControl.

Použijte podokno zdrojového kódu

V podokně Zdrojový kód se zobrazí zdrojové soubory použité při ověřování. Pokud je vybrán prvek v podokně Trace Tree , zdrojový kód soubor přidružený k prvku se zobrazí v horní části zásobníku souborů v sousedním podokně Zdrojový kód . Pokud chcete zobrazit jiný zdrojový soubor, klikněte na kartu zdrojového souboru v podokně Zdrojový kód .

Následující snímek obrazovky ukazuje podokno Zdrojový kód. V tomto podokně Zdrojový kód jsou řádky kódu zvýrazněné bledě modrými řádky, které jsou přidružené k vybranému prvku v podokně Trace Tree .

Řádky kódu ovladače, které jsou vykonány na cestě k vadě, jsou zobrazeny jako červený text. Když se podíváte jenom na řádky červeného textu, například řádek 116 a 118 v tomto příkladu, můžete někdy vidět vadu, zejména jednoduchou vadu, jako je ta, která se v tomto příkladu používá. V tomto případě ovladač získá zámek otáčení a pak se vrátí z rutiny dispečera bez uvolnění zámku otáčení.

Procházení trasování

Pokud chcete začít trasovat, vyberte prvek v podokně Trace Tree a stiskněte klávesu ŠIPKA DOLŮ. Pokaždé, když stisknete klávesu ŠIPKA DOLŮ, vybere se další prvek v podokně Trasovací strom .

Procházejte prvky v podokně Trasovací strom a sledujte podokno Zdrojový kód pro prvky pocházející z kódu ovladače. Pokud chcete rozbalit sbalený oddíl kódu, stiskněte klávesu ŠIPKA VPRAVO. Pokud chcete sbalit rozbalený oddíl kódu, stiskněte klávesu ŠIPKA VLEVO. Kurzor přeskočí všechny zavřené části kódu.

Při procházení prvků v podokně Trasovací strom se zdrojový soubor kódu, ve kterém vybraný prvek pochází, přesune na začátek zásobníku souborů v podokně Zdrojový kód a přidružený řádek kódu se zvýrazní.

Následující snímek obrazovky zobrazuje nástroj Static Driver Verifier Defect Viewer s podokny Trasovací strom a Zdrojový kód.

Použijte soubor pravidel a podokno stavu.

Podokno stavů můžete použít k zobrazení sady logických výrazů, které představují hodnoty proměnných, které SDV sleduje během ověřování.

Logické výrazy zobrazené v podokně Stav jsou ty z výrazy v sadě, které se vyhodnotí jako PRAVDA. Pokud prvek v podokně Trace Tree změní hodnotu libovolného výrazu, obsah podokna Stav se změní tak, aby se zobrazila nová sada výrazů, které se vyhodnotí jako TRUE.

Při procházení podokna Trasovací strom můžete sledovat, jak SDV používá hodnoty těchto proměnných k vyhodnocení výrazů použitých v souboru pravidel (*.slic).

Následující snímek obrazovky na stránce Sestava ověření statického ovladače ukazuje, jak testy SDV indikují, jestli ovladač předtím získal zámek otáčení. SDV testuje, zda ovladač předtím získal točivý zámek, tedy zda je hodnota proměnné s1, což znamená, že je uzamčený. V tomto případě s!=1 (odemčeno), jak je zobrazeno ve Stavovém podokně, takže SDV nastaví hodnotu s na 1, což znamená, že zámek je získán.

Najít rutinu ABORT

Pokud kód ovladače porušuje pravidlo, podokno Stromu trasování obsahuje rutinu ABORT pro hlášení chyby.

Pokud je cesta kódu k vadě dlouhá a složitá, je často užitečné se v podokně Stromu trasování posunout dolů, dokud nenajdete rutinu ABORT, a pak pomocí klávesy šipky nahoru vyhledejte kód, který bezprostředně spustil sestavu vad.

Například jak je znázorněno na následujícím snímku obrazovky, rutina ABORT je přidružena k řádku ze souboru CancelSpinLock.slic, který hlásí vadu po otestování, zda je zámek získán (s==locked). Test je součástí podprogramu, který se provádí při ukončení rutiny odeslání. Z těchto informací lze odvodit, že řidič neuspěl v uvolnění zámku otáčení před návratem z rutiny rozdělení.

Zavřete Prohlížeč chyb verifieru statického ovladače.

Jakmile identifikujete chybu kódu, která způsobila chybu, můžete zavřít okno Prohlížeče vad statického ovladače pro aktuální pravidlo a pak otevřít Prohlížeč vad pro jiné pravidlo.

Zavření Prohlížeče vad pro pravidlo:

• V nabídce Soubor vyberte Ukončit.

Můžete také kliknout na tlačítko Zavřít (X) pro Prohlížeč vad. Nachází se těsně pod tlačítkem Zavřít (X) pro sestavu ověření statického ovladače.

Následující snímek obrazovky ukazuje, jak zavřít Defect Viewer.