Het statische stuurprogramma-verifierrapport gebruiken

Het SDV-rapport is een interactieve weergave van de verificatieresultaten. In deze sectie wordt uitgelegd hoe u het SDV-rapport gebruikt om een coderingsfout in het stuurprogramma te vinden. Zie het static Driver Verifier-rapport voor gedetailleerde informatie over het rapport, de functies van de vensters en de elementen in de vensters.

De viewer voor defecten van statische stuurprogramma's openen

Als SDV eventuele 'defecten' (regelschendingen) in het deelvenster Resultaten heeft gerapporteerd, kunt u de code bekijken die betrokken is bij de schending in het venster Defect Viewer van het rapport Statische stuurprogrammaverificator. In het venster Defect Viewer wordt de code weergegeven in het pad naar de regelschending. Er is één venster Defect Viewer voor elke regel die is geschonden (u kunt slechts één venster Defect Viewer tegelijk weergeven).

Het venster Defect Viewer voor een defect openen:

• Selecteer een regel in de lijst onder het knooppunt Defect(en).

Deze procedure werkt alleen voor defecten. SDV genereert geen Defect Viewer venster als de resultaten van een verificatie geen defecten zijn, zoals slagen, time-outs, ruimte-overschrijdingen, niet van toepassing, of elk ander niet-defectresultaat.

In de volgende schermafbeelding ziet u een rapportpagina voor statische stuurprogrammaverificator.

De regel bekijken

Voordat u de schending van de regel in de code probeert te vinden, moet u bekend raken met de regels die het stuurprogramma heeft geschonden.

De sectie Regels voor statische stuurprogramma's bevat een onderwerp waarin elke regel wordt uitgelegd, bijvoorbeeld CancelSpinLock.

Als u de code voor de regel wilt zien, klikt u in het deelvenster Broncode van het statische stuurprogrammaverifier-rapport op het tabblad met de regelcode, zoals CancelSpinLock.slic.

De regel CancelSpinLock wordt bijvoorbeeld geschonden als het stuurprogramma IoAcquireCancelSpinLock of IoReleaseCancelSpinLock buiten orde aanroept, of als het stuurprogramma de routine verlaat voordat het kringslot wordt losgelaten.

Het pad naar defect traceren

Wanneer het venster Defect Viewer wordt geopend, wordt het element in het deelvenster Traceringsstructuur dat de eerste kritieke stuurprogramma-aanroep in het pad naar het defect vertegenwoordigt geselecteerd. In het deelvenster Broncode is de bijbehorende regel broncode blauw gemarkeerd.

In de volgende schermafbeelding ziet u de openingsweergave van het venster Static Driver Verifier Defect Viewer voor een schending van de regel CancelSpinLock door het Fail_Driver1 voorbeeldstuurprogramma. In dit voorbeeld is de eerste aanroep van het stuurprogramma in het pad naar een schending van de regel CancelSpinLock een aanroep naar IoAcquireCancelSpinLock in de DispatchSystemControl-routine van het stuurprogramma.

Het deelvenster Broncode gebruiken

In het deelvenster Broncode worden de bronbestanden weergegeven die in de verificatie worden gebruikt. Wanneer een element in het deelvenster Traceringsstructuur is geselecteerd, wordt het broncodebestand dat is gekoppeld aan het element boven aan de bestandsstack weergegeven in het aangrenzende deelvenster Broncode . Als u een ander bronbestand wilt zien, klikt u op het tabblad voor het bronbestand in het deelvenster Broncode .

In de volgende schermafbeelding ziet u het deelvenster Broncode. In dit deelvenster Broncode zijn de regels code die lichtblauw gemarkeerd zijn, gekoppeld aan het geselecteerde element in het deelvenster Traceringsstructuur.

De regels in de stuurprogrammacode die worden uitgevoerd in het pad naar het defect, worden weergegeven in rode tekst. Door alleen naar de regels met rode tekst te kijken, zoals regel 116 en 118 in dit voorbeeld, kunt u soms het defect zien, met name een eenvoudig defect zoals in dit voorbeeld. In dit geval verkrijgt de bestuurder de spinvergrendeling en keert deze vervolgens terug uit de verzendroutine zonder de spinvergrendeling los te laten.

Loop door de trace

Als u wilt beginnen met traceren, selecteert u een element in het paneel Traceerstructuur en drukt u vervolgens op de toets PIJL-OMLAAG. Telkens wanneer u op de pijl-omlaag drukt, wordt het volgende element in het deelvenster Trace Tree geselecteerd.

Terwijl u de elementen in het deelvenster Traceringsstructuur doorloopt, bekijkt u het deelvenster Broncode voor elementen uit de stuurprogrammacode. Als u een ingeklapte code wilt uitvouwen, drukt u op de pijltje naar rechts-toets. Druk op de pijl-links om een uitgevouwen codegedeelte in te klappen. Met de cursor worden alle samengevouwen codesecties overgeslagen.

Wanneer u omlaag schuift door de elementen in het deelvenster Traceringsstructuur , wordt het broncodebestand waarin het geselecteerde element afkomstig is, verplaatst naar de bovenkant van de stapel bestanden in het deelvenster Broncode en wordt de bijbehorende coderegel gemarkeerd.

In de volgende schermafbeelding is de Static Driver Verifier Defect Viewer te zien met de panelen Trace Tree en Source Code.

Gebruik het Regelbestand- en Statusdeelvenster

U kunt het deelvenster Status gebruiken om de set Booleaanse expressies weer te geven die de waarden vertegenwoordigen van variabelen die SDV tijdens de verificatie bijhoudt.

De Boole-expressies die worden weergegeven in het deelvenster Status zijn de expressies in die set die resulteren in WAAR. Als het element in het deelvenster Traceringsstructuur de waarde van een expressie wijzigt, wordt de inhoud van het deelvenster Status gewijzigd om de nieuwe set expressies weer te geven die resulteren in WAAR.

Wanneer u het deelvenster Traceringsstructuur doorloopt, kunt u zien hoe SDV de waarden van deze variabelen gebruikt om de expressies te evalueren die in het regelsbestand (*.slic) worden gebruikt.

In de volgende schermafbeelding van de pagina Static Driver Verifier Report ziet u hoe SDV-tests aangeven of het stuurprogramma eerder een spinvergrendeling had verkregen. SDV test om te zien of het stuurprogramma eerder een spinvergrendeling had verkregen, dat wil zeggen, als de waarde van de variabele s1 is, wat betekent dat het vergrendeld is. In dit geval is s!=1 (ontgrendeld), zoals weergegeven in het deelvenster Staat, dus stelt SDV de waarde van s in op 1, wat aangeeft dat de vergrendeling is verkregen.

De ABORT Routine zoeken

Wanneer de stuurprogrammacode een regel schendt, bevat het deelvenster Traceringsstructuur een ABORT-routine voor het rapporteren van het defect.

Wanneer het codepad naar een defect lang en complex is, is het vaak handig om omlaag te schuiven in het deelvenster Traceringsstructuur totdat u de ABORT-routine hebt gevonden en gebruik vervolgens de toets PIJL-OMHOOG om de code te vinden die het defectrapport het meest onmiddellijk heeft geactiveerd.

Zoals in de volgende schermafbeelding wordt weergegeven, wordt de ABORT-routine bijvoorbeeld gekoppeld aan een regel uit het bestand CancelSpinLock.slic dat het defect rapporteert na het testen of de vergrendeling is verkregen (s==vergrendeld). De test maakt deel uit van een subroutine die wordt uitgevoerd wanneer de verzendroutine afloopt. Uit deze informatie kunt u afleiden dat de bestuurder geen spinvergrendeling loslaat voordat hij terugkeert uit de verzendroutine.

De viewer voor defecten van statische stuurprogramma's sluiten

Nadat u de codefout hebt geïdentificeerd die het defect heeft veroorzaakt, kunt u het venster Static Driver Verifier Defect Viewer voor de huidige regel sluiten en vervolgens de Viewer voor defecten openen voor een andere regel.

De defectviewer voor een regel sluiten:

• Selecteer in het Bestand menu Afsluiten.

U kunt ook op de knop Sluiten (X) klikken voor de Defect Viewer. Het bevindt zich net onder de knop Sluiten (X) voor het statische stuurprogramma verifier-rapport.

In de volgende schermafbeelding ziet u hoe u de Defect Viewer sluit.