Penggunaan Laporan Pemverifikasi Driver Statis

Laporan SDV adalah tampilan interaktif dari hasil verifikasi. Bagian ini menjelaskan cara menggunakan Laporan SDV untuk menemukan kesalahan pengkodian di driver. Untuk informasi terperinci tentang laporan, fitur jendela, dan elemen di jendela, lihat Laporan Pemverifikasi Driver Statis.

Buka Penampil Cacat Pemverifikasi Driver Statis

Jika SDV melaporkan "cacat" (pelanggaran aturan) di panel Hasil , Anda dapat melihat kode yang terlibat dalam pelanggaran di jendela Penampil Cacat dari Laporan Pemverifikasi Driver Statis. Jendela Peninjau Cacat menampilkan kode dalam jalur menuju pelanggaran aturan. Ada satu jendela Penampil Cacat untuk setiap aturan yang dilanggar (Anda hanya dapat melihat satu jendela Penampil Cacat pada satu waktu).

Untuk membuka jendela Penampil Cacat terkait cacat:

• Pilih aturan dari daftar di bawah simpul Cacat .

Prosedur ini hanya berfungsi untuk kerusakan. SDV tidak menghasilkan jendela Penampil Cacat jika hasil verifikasi bukan cacat, seperti lulus, timeout, pengosongan, tidak berlaku, atau hasil lain yang bukan cacat.

Cuplikan layar berikut menunjukkan halaman Laporan Pemverifikasi Driver Statis.

Tinjau Aturan

Sebelum mencoba menemukan pelanggaran aturan dalam kode, kenali aturan yang dilanggar driver.

Bagian Aturan Pemverifikasi Driver Statis menyertakan topik yang menjelaskan setiap aturan, misalnya, CancelSpinLock.

Untuk melihat kode untuk aturan, di panel Kode Sumber dari Laporan Pemverifikasi Driver Statis, klik tab dengan kode aturan, seperti CancelSpinLock.slic.

Misalnya, aturan CancelSpinLock dilanggar jika driver memanggil IoAcquireCancelSpinLock atau IoReleaseCancelSpinLock di luar urutan, atau jika driver keluar dari rutinitas sebelum melepaskan kunci putar.

Lacak Jalur Cacat

Saat jendela Penampil Cacat terbuka, elemen di panel Lacak Pohon yang mewakili panggilan driver penting pertama di jalur cacat dipilih. Di panel Kode Sumber , baris kode sumber terkait disorot dengan warna biru.

Cuplikan layar berikut menunjukkan tampilan pembuka jendela Penampil Cacat Pemverifikasi Driver Statis untuk pelanggaran aturan CancelSpinLock oleh driver sampel Fail_Driver1. Dalam contoh ini, panggilan driver pertama di jalur menuju pelanggaran aturan CancelSpinLock adalah panggilan ke IoAcquireCancelSpinLock dalam rutin DispatchSystemControl driver.

Menggunakan Panel Kode Sumber

Panel Kode Sumber menampilkan file sumber yang digunakan dalam verifikasi. Saat elemen di panel Lacak Pohon dipilih, file kode sumber yang terkait dengan elemen muncul di bagian atas tumpukan file di panel Kode Sumber yang berdekatan. Untuk melihat file sumber lain, klik tab untuk file sumber di panel Kode Sumber .

Cuplikan layar berikut ini memperlihatkan panel Kode Sumber. Di panel Kode Sumber ini, baris kode yang disorot dengan warna biru pucat adalah baris yang terkait dengan elemen yang dipilih di panel Lacak Pohon .

Baris dalam kode driver yang dijalankan di jalur menuju cacat ditampilkan dengan teks berwarna merah. Dengan hanya melihat baris teks merah, seperti baris 116 dan 118 dalam contoh ini, Anda kadang-kadang dapat melihat cacat, terutama cacat sederhana seperti yang digunakan dalam contoh ini. Dalam hal ini, driver memperoleh kunci putaran, dan kemudian kembali dari rutinitas pengiriman tanpa melepaskan kunci putaran.

Langkah-Langkah Menelusuri Jejak

Untuk mulai melacak, pilih elemen di panel Pohon Penelusuran, lalu tekan tombol PANAH BAWAH. Setiap kali Anda menekan PANAH BAWAH, elemen berikutnya di panel Pohon Jejak akan dipilih.

Saat Anda menelusuri elemen di panel Lacak Pohon , tonton panel Kode Sumber untuk elemen dari kode driver. Untuk memperluas bagian kode yang diciutkan, tekan tombol PANAH KANAN. Untuk menutup bagian kode yang diperluas, tekan tombol PANAH KIRI. Kursor mengabaikan semua bagian kode yang diciutkan.

Saat Anda menggulir ke bawah melalui elemen di panel Pohon Jejak , file kode sumber tempat elemen yang dipilih berasal berpindah ke bagian atas tumpukan file di panel Kode Sumber dan baris kode terkait disorot.

Cuplikan layar berikut menunjukkan tampilan Static Driver Verifier Defect Viewer dengan panel Pohon Jejak dan Kode Sumber.

Menggunakan File Aturan dan Panel Status

Anda bisa menggunakan Panel Status untuk melihat kumpulan ekspresi Boolean yang mewakili nilai variabel yang dilacak SDV selama verifikasi.

Ekspresi Boolean yang ditampilkan di panel Status adalah ekspresi dalam kumpulan yang dievaluasi ke TRUE. Jika elemen di panel Pohon Pelacakan mengubah nilai ekspresi apa pun, konten panel Status berubah untuk menampilkan kumpulan ekspresi baru yang mengevaluasi ke TRUE.

Saat Menelusuri panel Pohon Jejak , Anda dapat mengamati bagaimana SDV menggunakan nilai variabel ini untuk mengevaluasi ekspresi yang digunakan dalam file aturan (*.slic).

Tangkapan layar dari halaman Laporan Verifier Driver Statis berikut menunjukkan bagaimana pengujian SDV mengindikasikan apakah driver sebelumnya telah memperoleh kunci putar. SDV menguji untuk melihat apakah driver sebelumnya telah memperoleh kunci putaran, yaitu jika nilai variabel s adalah 1, yang berarti terkunci. Dalam hal ini, s!=1 (tidak terkunci), seperti yang ditampilkan di panel Status, sehingga SDV mengatur nilai s ke 1, menunjukkan bahwa kunci diperoleh.

Temukan Rutinitas ABORT

Saat kode driver melanggar aturan, panel Pohon Jejak berisi rutinitas ABORT untuk melaporkan cacat.

Ketika jalur kode ke bug panjang dan kompleks, sering kali berguna untuk menggulir ke bawah di panel Pohon Jejak sampai Anda menemukan rutinitas ABORT, lalu gunakan tombol PANAH ATAS untuk menemukan kode yang langsung memicu laporan bug.

Misalnya, seperti yang ditunjukkan pada cuplikan layar berikut, rutinitas ABORT dikaitkan dengan baris dari file CancelSpinLock.slic yang melaporkan cacat setelah menguji apakah kunci diperoleh (s==terkunci). Pengujian ini adalah bagian dari subroutine yang dilakukan ketika rutinitas pengiriman berakhir. Dari informasi ini, Anda dapat menyimpulkan bahwa driver gagal melepaskan kunci putaran sebelum kembali dari rutinitas pengiriman.

Menutup Penampil Kesalahan Pemverifikasi Driver Statis

Setelah mengidentifikasi kesalahan kode yang menyebabkan cacat, Anda dapat menutup jendela Penampil Cacat Pemverifikasi Driver Statis untuk aturan saat ini, lalu membuka Penampil Cacat untuk aturan yang berbeda.

Untuk menutup Penampil Cacat untuk suatu aturan:

• Dari menu File , pilih Keluar.

Anda juga dapat mengklik tombol Tutup (X) untuk Penampil Cacat. Ini terletak tepat di bawah tombol Tutup (X) untuk Laporan Pemverifikasi Driver Statis.

Cuplikan layar berikut menunjukkan cara menutup Penampil Cacat.