Uso del informe comprobador de controladores estáticos
El informe de SDV es una presentación interactiva de los resultados de la comprobación. En esta sección se explica cómo usar el informe de SDV para buscar un error de codificación en el controlador. Para obtener información detallada sobre el informe, las características de las ventanas y los elementos de las ventanas, vea Static Driver Verifier Report.
Abrir el Visor de defectos del comprobador de controladores estáticos
Si SDV notificó "defectos" (infracciones de reglas) en el panel Resultados , puede ver el código implicado en la infracción en la ventana Visor de defectos del informe comprobador de controladores estáticos. La ventana Visor de defectos muestra el código en la ruta de acceso a la infracción de la regla. Hay una ventana visor de defectos para cada regla que se infringió (solo puede ver una ventana visor de defectos cada vez).
Para abrir la ventana Visor de defectos para un defecto:
- Seleccione una regla de la lista en el nodo Defectos .
Este procedimiento solo funciona para defectos. SDV no genera una ventana visor de defectos si los resultados de una comprobación no son defectos, como pases, tiempos de espera, espaciaciones, no aplicables o cualquier otro resultado no defectuoso.
En la captura de pantalla siguiente se muestra una página de informe del comprobador de controladores estáticos.
Revisar la regla
Antes de intentar encontrar la infracción de regla en el código, familiarícese con las reglas que infringía el controlador.
La sección Reglas del comprobador de controladores estáticos incluye un tema que explica cada regla, por ejemplo , CancelSpinLock.
Para ver el código de la regla, en el panel Código fuente del informe comprobador de controladores estáticos, haga clic en la pestaña con el código de regla, como CancelSpinLock.slic.
Por ejemplo, se infringe la regla CancelSpinLock si el controlador llama a IoAcquireCancelSpinLock o IoReleaseCancelSpinLock fuera de orden, o si el controlador sale de la rutina antes de liberar el bloqueo de giro.
Seguimiento de la ruta de acceso del defecto
Cuando se abre la ventana Visor de defectos , se selecciona el elemento del panel Árbol de seguimiento que representa la primera llamada de controlador crítica en la ruta de acceso a defectos. En el panel Código fuente , la línea de código fuente asociada se resalta en azul.
En la captura de pantalla siguiente se muestra la vista de apertura de la ventana Visor de defectos del comprobador de controladores estáticos para una infracción de la regla CancelSpinLock por parte del controlador de ejemplo de Fail_Driver1. En este ejemplo, la primera llamada del controlador en la ruta de acceso a una infracción de la regla CancelSpinLock es una llamada a IoAcquireCancelSpinLock en la rutina DispatchSystemControl del controlador.
Usar el panel de código fuente
En el panel Código fuente se muestran los archivos de origen usados en la comprobación. Cuando se selecciona un elemento en el panel Árbol de seguimiento , el archivo de código fuente asociado al elemento aparece en la parte superior de la pila de archivos en el panel Código fuente adyacente. Para ver un archivo de origen diferente, haga clic en la pestaña del archivo de origen en el panel Código fuente .
En la captura de pantalla siguiente se muestra el panel Código fuente. En este panel Código fuente , las líneas de código resaltadas en azul pálido son las que están asociadas al elemento seleccionado en el panel Árbol de seguimiento .
Las líneas del código de controlador que se ejecutan en la ruta de acceso al defecto se muestran en texto rojo. Al examinar solo las líneas de texto rojo, como la línea 116 y 118 en este ejemplo, a veces puede ver el defecto, especialmente un defecto simple como el usado en este ejemplo. En este caso, el controlador adquiere el bloqueo de giro y, a continuación, vuelve de la rutina de envío sin liberar el bloqueo de giro.
Recorrer paso a paso el seguimiento
Para comenzar el seguimiento, seleccione un elemento en el panel Árbol de seguimiento y presione la tecla FLECHA ABAJO. Cada vez que presione FLECHA ABAJO, se selecciona el siguiente elemento del panel Árbol de seguimiento .
A medida que recorra los elementos del panel Árbol de seguimiento, watch el panel Código fuente de los elementos del código de controlador. Para expandir una sección contraída del código, presione la tecla FLECHA DERECHA. Para contraer una sección expandida del código, presione la tecla FLECHA IZQUIERDA. El cursor omite todas las secciones contraídas del código.
A medida que se desplaza hacia abajo por los elementos del panel Árbol de seguimiento, el archivo de código fuente en el que se origina el elemento seleccionado se mueve a la parte superior de la pila de archivos en el panel Código fuente y se resalta la línea de código asociada.
En la captura de pantalla siguiente se muestra el Visor de defectos del comprobador de controladores estáticos con los paneles Árbol de seguimiento y Código fuente.
Usar el archivo de reglas y el panel de estado
Puede usar el panel de estado para ver el conjunto de expresiones booleanas que representan los valores de las variables que realiza el seguimiento de SDV durante la comprobación.
Las expresiones booleanas que se muestran en el panel Estado son las expresiones de ese conjunto que se evalúan como TRUE. Si el elemento del panel Árbol de seguimiento cambia el valor de cualquier expresión, el contenido del panel Estado cambia para mostrar el nuevo conjunto de expresiones que se evalúan como TRUE.
Al recorrer el panel Árbol de seguimiento , puede observar cómo SDV usa los valores de estas variables para evaluar las expresiones usadas en el archivo de reglas (*.slic).
La siguiente captura de pantalla de la página Informe del comprobador de controladores estáticos muestra cómo las pruebas de SDV indican si el controlador había adquirido previamente un bloqueo de giro. SDV comprueba si el controlador había adquirido previamente un bloqueo de giro, es decir, si el valor de la variable s es 1, lo que significa bloqueado. En este caso, s!=1 (desbloqueado), tal como se muestra en el panel Estado, por lo que SDV establece el valor de s en 1, lo que indica que se adquiere el bloqueo.
Buscar la rutina ABORT
Cuando el código del controlador infringe una regla, el panel Árbol de seguimiento contiene una rutina ABORT para notificar el defecto.
Cuando la ruta de acceso del código a un defecto es larga y compleja, a menudo resulta útil desplazarse hacia abajo en el panel Árbol de seguimiento hasta encontrar la rutina ABORT y, a continuación, usar la tecla FLECHA ARRIBA para encontrar el código que más inmediatamente desencadenó el informe de defectos.
Por ejemplo, como se muestra en la siguiente captura de pantalla, la rutina ABORT está asociada a una línea del archivo CancelSpinLock.slic que informa del defecto después de probar si el bloqueo se adquiere (s==locked). La prueba forma parte de una subrutina que se realiza cuando finaliza la rutina de envío. A partir de esta información, puede deducir que el controlador no pudo liberar un bloqueo de giro antes de volver de la rutina de envío.
Cerrar el Visor de defectos del comprobador de controladores estáticos
Después de identificar el error de código que causó el defecto, puede cerrar la ventana Visor de defectos del comprobador de controladores estáticos para la regla actual y, a continuación, abrir el Visor de defectos para una regla diferente.
Para cerrar el Visor de defectos de una regla:
- En el menú Archivo , seleccione Salir.
También puede hacer clic en el botón Cerrar (X) para el Visor de defectos. Se encuentra justo debajo del botón Cerrar (X) para el informe comprobador de controladores estáticos.
En la captura de pantalla siguiente se muestra cómo cerrar el Visor de defectos.
