Diferencias entre Polyspace Bug Finder y Polyspace Code Prover
Polyspace® Bug Finder™ y Polyspace Code Prover™ detectan errores en tiempo de ejecución mediante análisis estáticos. Aunque los productos tienen una interfaz de usuario similar y las matemáticas subyacentes al análisis pueden en ocasiones ser las mismas, los objetivos de los dos productos son diferentes.
Bug Finder (o Polyspace as You Code, que realiza un análisis de un solo archivo similar a Bug Finder) analiza rápidamente el código y detecta muchos tipos de defectos. Code Prover comprueba todas las operaciones del código para detectar un conjunto de posibles errores en tiempo de ejecución e intenta probar la ausencia de errores en todas las rutas de ejecución.
Nota
Para cada operación del código, Code Prover tiene en cuenta todas las rutas de ejecución que conducen a la operación y que no tienen un error anterior. Si una ruta de ejecución contiene un error anterior a la operación, Code Prover no la tiene en cuenta. Consulte Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).
Por ejemplo, para cada división del código, un análisis de Code Prover intenta probar que el denominador no puede ser cero. Bug Finder no realiza verificaciones tan exhaustivas. Por ejemplo, Bug Finder también comprueba los errores de división por cero, pero puede no encontrar todas las operaciones que causen el error.
Los dos productos presentan diferencias de configuración, análisis y revisión de resultados, derivadas de esta diferencia en objetivos. En las siguientes secciones, destacamos las principales diferencias entre un análisis de Bug Finder y de Code Prover (también conocido como verificación). En función de los requisitos, puede incorporar uno o ambos tipos de análisis en momentos adecuados del ciclo de vida del desarrollo de software.
Visión general de las diferencias entre Bug Finder y Code Prover
Utilice tanto Bug Finder como Code Prover regularmente en el proceso de desarrollo. Estos productos proporcionan un conjunto único de prestaciones y se complementan entre sí. Para obtener más información sobre posibles maneras de utilizar los productos conjuntamente, consulte Flujo de trabajo usando tanto Polyspace Bug Finder como Polyspace Code Prover.
Esta tabla proporciona una visión general de cómo los productos se complementan entre sí. Para obtener más información, consulte las secciones que aparecen a continuación.
| Funcionalidad | Bug Finder | Code Prover |
|---|---|---|
| Número de comprobadores | Más de 300 comprobadores de defectos | 30 comprobaciones de errores críticos en tiempo de ejecución y 4 comprobaciones de uso global de variables |
| Profundidad del análisis | Rápido. Por ejemplo:
| Exhaustivo. Por ejemplo:
|
| Criterios de creación de informes | Defectos probables | Conclusiones probadas |
| Criterios de búsqueda de bugs | Algunos falsos positivos | Ningún falso negativo |
Cómo Bug Finder y Code Prover se complementan entre sí
Análisis más rápido con Bug Finder
La velocidad del análisis de Bug Finder depende del tamaño de la aplicación. El tiempo de análisis de Bug Finder aumenta linealmente con el tamaño de la aplicación. El tiempo de verificación de Code Prover aumenta a un ritmo más rápido que el lineal.
Un flujo de trabajo posible consiste en ejecutar Code Prover para analizar la solidez de módulos o bibliotecas frente a determinados errores y ejecutar Bug Finder en la fase de integración. El análisis de Bug Finder de bases de código grandes puede completarse en un tiempo mucho menor y también se encuentran defectos de integración como Declaration mismatch y Data race.
Verificación más exhaustiva con Code Prover
Code Prover intenta probar la ausencia de:
Errores Division by Zero en todas las divisiones y operaciones del módulo
Errores Out of Bounds Array Index en todos los accesos de arreglos
Errores Non-initialized Variable en todas las lecturas de variables
Errores Overflow en todas las operaciones que pueden desbordarse
etc.
Para cada operación:
Si Code Prover puede probar la ausencia del error para todas las rutas de ejecución, resalta la operación en verde.
Si Code Prover puede probar la presencia de un error definido para todas las rutas de ejecución, resalta la operación en rojo.
Si Code Prover no puede probar la ausencia de un error o la presencia de un error definido, resalta la operación en naranja. El bajo porcentaje de comprobaciones en naranja indica operaciones que debe revisar cuidadosamente, mediante inspección visual o pruebas. Las comprobaciones en naranja normalmente indican vulnerabilidades ocultas. Por ejemplo, es posible que la operación sea segura en el contexto actual, pero que falle si se reutiliza en otro contexto.
Puede utilizar la información proporcionada por la interfaz de usuario de Polyspace para diagnosticar las comprobaciones. Consulte Análisis más rigurosos de estructuras de control y flujos de datos con Code Prover. También puede proporcionar información contextual para reducir aún más el código no probado, por ejemplo, restringiendo los rangos de entrada externamente.
Bug Finder no está diseñado para realizar un análisis exhaustivo. Intenta detectar tantos bugs como sea posible y reducir los falsos positivos. Para componentes de software críticos, no es suficiente con ejecutar una herramienta de búsqueda de bugs, ya que, aunque se corrijan todos los defectos encontrados en el análisis, aún puede haber errores durante la ejecución del código (falsos negativos). Después de ejecutar Code Prover en el código y resolver los problemas encontrados, la calidad del código mejorará significativament. Consulte Ningún falso negativo con Code Prover.
Tipos de defectos más específicos con Bug Finder
Code Prover comprueba si hay tipos de errores en tiempo de ejecución donde sea matemáticamente posible probar la ausencia del error. Además de detectar errores cuya ausencia pueda probarse matemáticamente, Bug Finder también detecta otros defectos.
Por ejemplo, la instrucción if(a=b) es semánticamente correcta según el estándar del lenguaje C, pero normalmente indica una asignación no deseada. Bug Finder detecta ese tipo de operaciones no deseadas. Aunque Code Prover no detecta este tipo de operaciones no deseadas, puede detectar si una operación no deseada causa otros errores en tiempo de ejecución.
Los ejemplos de defectos detectados por Bug Finder, pero no por Code Prover incluyen defectos de buenas prácticas, defectos de gestión de recursos, algunos defectos de programación, defectos de seguridad y defectos en el diseño orientado a objetos C++.
Para obtener más información, consulte:
Defectos: lista de defectos detectados por Bug Finder.
Run-Time Checks (Polyspace Code Prover): lista de errores en tiempo de ejecución detectados por Code Prover.
Proceso de configuración más sencillo con Bug Finder
Aunque el código se compile satisfactoriamente en la cadena de herramientas de compilación, puede fallar en la fase de compilación de una verificación de Code Prover. La compilación estricta de Code Prover está relacionada con su habilidad para probar la ausencia de determinados errores en tiempo de ejecución.
Code Prover sigue estrictamente el estándar ANSI® C99, a menos que utilice explícitamente opciones de análisis que emulen su compilador.
Para permitir desviaciones del estándar ANSI C99, deberá utilizar las opciones Objetivo y compilador. Si crea un proyecto de Polyspace desde el sistema de compilación, las opciones se ajustan automáticamente.
Code Prover no admite errores de enlace que los compiladores habituales pueden permitir.
Aunque el compilador permita errores de enlace, como la discordancia en la firma de función entre unidades de compilación, para evitar un comportamiento inesperado en el tiempo de ejecución, deberá corregir los errores.
Para obtener más información, consulte Troubleshoot Compilation and Linking Errors (Polyspace Code Prover).
Bug Finder es menos estricto en relación con determinados errores de compilación. Los errores de enlace, como la discordancia en la firma de función entre unidades de compilación, pueden detener una verificación de Code Prover, pero no un análisis de Bug Finder. Por ello, puede ejecutar un análisis de Bug Finder con menos esfuerzo de configuración. En Bug Finder, los errores de enlace se suelen notificar como defecto una vez completado el análisis.
Menos ejecuciones para un código limpio con Bug Finder
Para garantizar la ausencia de determinados errores en tiempo de ejecución, Code Prover sigue unas reglas estrictas cuando detecta un error en tiempo de ejecución en una operación. Cuando se produce un error en tiempo de ejecución, el estado del programa está mal definido y Code Prover no puede probar la ausencia de errores en el código posterior. Por ello:
Si Code Prover prueba un error definido y muestra una comprobación en rojo, no verifica el resto del código del mismo bloque.
Las excepciones incluyen comprobaciones como Overflow, donde el análisis continúa con el resultado del desbordamiento truncado o envuelto.
Si Code Prover sospecha que existe un error y muestra una comprobación en naranja, ya no tiene en cuenta la ruta que contiene el error. Por ejemplo, si Code Prover detecta un error Division by Zero en la operación
1/x, en la operación siguiente enxde ese bloque,xno puede ser cero.Si Code Prover detecta que no puede acceder a un bloque de código y muestra una comprobación en gris, no detecta errores en ese bloque.
Para obtener más información, consulte Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).
Por ello, cuando corrija las comprobaciones en rojo y gris, y vuelva a ejecutar la verificación, puede encontrar más problemas. Es necesario ejecutar la verificación varias veces y corregir los problemas cada vez para obtener un código completamente limpio. La situación es similar a las pruebas dinámicas. En las pruebas dinámicas, cuando se corrige un error en un punto determinado del código, puede descubrir un error nuevo en el código posterior.
Bug Finder no detiene el análisis completo de un bloque después de encontrar un defecto en ese bloque. Con Bug Finder, también puede ser necesario ejecutar el análisis varias veces para obtener un código completamente limpio. No obstante, el número de ejecuciones requeridas es menor que en Code Prover.
Resultados en tiempo real con Bug Finder
Bug Finder muestra algunos resultados mientras el análisis sigue ejecutándose. No es necesario esperar hasta el final del análisis para revisar los resultados.
Code Prover solo muestra los resultados después de que haya finalizado la verificación. Cuando Bug Finder encuentra un defecto, lo puede mostrar. Code Prover debe probar la ausencia de errores en todas las rutas de ejecución. Por ello, no puede mostrar resultados durante el análisis.
Análisis más rigurosos de estructuras de control y flujos de datos con Code Prover
Para cada operación del código, Code Prover proporciona:
Recuadros que muestran el intervalo de valores de cada variable en la operación.
En un puntero, los recuadros muestran la variable que el puntero señala, junto con los valores de la variable.
Representación gráfica de la secuencia de llamada a la función que conduce a la operación.
Utilizando esta información sobre intervalos y la gráfica de llamadas, puede navegar fácilmente por la jerarquía de llamadas a funciones y comprender cómo una variable adquiere valores que provocan un error. Por ejemplo, para un error Out of Bounds Array Index, puede encontrar el lugar en el que a la variable de índice se le asignan por primera vez valores que provocan el error.
Cuando revisa resultados en Bug Finder, también dispone de información auxiliar para comprender la causa raíz de un defecto. Por ejemplo, puede rastrear la causa raíz de un defecto desde el lugar donde Bug Finder lo encontró. No obstante, en Code Prover dispone de información más completa, ya que la información permite entender todas las rutas de ejecución del código.
Análisis de flujos de datos en Code Prover
Análisis de estructuras de control en Code Prover
Pocos falsos positivos con Bug Finder
Bug Finder aspira a detectar menos falsos positivos, es decir, resultados que es probable que no corrija. De forma predeterminada, solo se muestran los defectos que probablemente resulten más significativos.
Bug Finder también asigna un atributo llamado impacto a los tipos de defectos según la gravedad de los defectos y la tasa de falsos positivos. Puede decidir analizar el código solo en busca de defectos de gran impacto. También puede activar o desactivar un defecto que no desea revisar.
Asimismo, puede desactivar determinados defectos de Code Prover relacionados con la no inicialización.
Ningún falso negativo con Code Prover
Code Prover aspira a realizar un análisis exhaustivo. El software comprueba todas las operaciones que pueden provocar tipos de error específicos. Si una operación de código es verde, significa que la operación no puede provocar esos errores en tiempo de ejecución que el software ha comprobado. De esta forma, el software aspira a no emitir ningún falso negativo.
El resultado de Code Prover solo es válido si se ejecuta el código en las mismas condiciones que indicó en Code Prover por medio de las opciones de análisis.
Si el software no puede probar la ausencia de un error, resalta la operación sospechosa en rojo o naranja y requiere que la revise.
Compatibilidad con reglas de codificación en Bug Finder
Bug Finder permite comprobar el cumplimiento de estándares de codificación externos, como:
AUTOSAR C++14. Consulte Reglas AUTOSAR C++14.
MISRA C:2012. Consulte Directrices y reglas de MISRA C:2012.
MISRA C++:2008. Consulte Reglas MISRA C++:2008.
CERT C. Consulte Reglas y recomendaciones CERT C.
CERT C++. Consulte Reglas CERT C++.
Para ver una lista completa de los estándares de codificación compatibles, consulte Polyspace Support for Coding Standards.
Consulte también
Temas
- Workflow Using Both Polyspace Bug Finder and Polyspace Code Prover (Polyspace Code Prover)
