Panel Keadaan

Panel Status menampilkan ekspresi Boolean untuk nilai variabel dalam driver, model sistem operasi, dan aturan. SDV menggunakan ekspresi ini untuk membangun abstraksi driver, model sistem operasi, dan aturan, dan menggunakannya dalam verifikasi.

Cuplikan layar berikut ini memperlihatkan contoh panel Status di Penampil Cacat.

Panel Status adalah komponen penampil Cacat. Saat elemen kode disorot di panel Pohon Jejak, dan baris kode sumber yang sesuai disorot di panel Kode Sumber, panel Status menampilkan ekspresi Boolean (dari kumpulan ekspresi yang dilacak SDV untuk driver) yang mengevaluasi ke TRUE sebelum baris kode dijalankan.

Melacak Ekspresi Boolean

Saat memverifikasi setiap aturan untuk pengemudi, SDV melacak serangkaian pernyataan Boolean. 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.

Menginterpretasikan Ekspresi di Panel Status

Sebagian besar ekspresi yang muncul di panel Status terkait dengan variabel yang terbukti dalam kode aturan. Anda dapat menggunakan kode sumber untuk aturan (dalam file RuleName.slic di panel Kode Sumber ) untuk membantu Anda menginterpretasikan ekspresi.

Namun, beberapa ekspresi muncul di panel Status tanpa detail tentang representasi internalnya yang mungkin membantu Anda menginterpretasikannya. Contohnya,

x!=x

Untuk SDV, ekspresi ini mewakili kondisi di mana nilai variabel x pada titik ini dalam jejak tidak sama dengan nilai variabel yang sama pada titik yang berbeda dalam jejak. Gunakan kode sumber driver, kode aturan (*.slic), dan elemen di panel Pohon Jejak untuk membantu Anda menafsirkan ekspresi.

Tab Langkah di Panel Status

Ekspresi Boolean di panel Status ditampilkan pada tab. Setiap tab mewakili langkah dalam jejak melalui semua kode sumber yang digunakan dalam verifikasi. Angka pada tab langkah menunjukkan urutan langkah tersebut dalam pelacakan.

Biasanya, karena setiap baris kode sumber hanya mewakili satu langkah dalam pelacakan, hanya akan ada satu tab langkah di panel Status . Namun, kode kompleks dapat menghasilkan banyak langkah.

Misalnya, cuplikan layar berikut menunjukkan panel Status yang menampilkan baris kode yang menyertakan penunjuk fungsi. Dalam hal ini, setiap tab mewakili langkah dalam resolusi penunjuk, pemanggilan fungsi yang ditunjuk, dan hasilnya. (Jumlah tab langkah mengungkapkan berapa banyak langkah yang diperlukan SDV untuk menyelesaikan penunjuk fungsi.)

Untuk menampilkan setiap tab langkah di panel Status secara berurutan, pilih baris kode terkait di panel Kode Sumber . Kemudian, klik baris kode di panel Kode Sumber berulang kali. Setiap kali Anda mengklik baris kode yang dipilih, SDV menampilkan tab langkah berikutnya hingga Anda menelusuri semua tab langkah. Panah kuning melengkung menunjukkan langkah yang dipilih.

Anda juga bisa mengklik tab apa pun di panel Status untuk menampilkan kontennya.

Komentar

SDV sering melacak ekspresi di panel Status yang tidak muncul dalam aturan dan tampaknya tidak terkait langsung dengan aturan. Ekspresi ini dihasilkan dari heuristik canggih yang digunakan SDV dalam upayanya untuk menghubungkan nilai yang berbeda dan pelanggaran aturan yang berbeda. Dalam beberapa situasi, SDV tidak dapat mengevaluasi ekspresi dengan benar. Dalam kasus ini, SDV memberikan pesan yang menyatakan bahwa status saat ini tidak diketahui, dan menampilkan ekspresi dari langkah yang memiliki status terakhir yang diketahui. Lihat, contoh kode berikut untuk penjelasan:

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