Différences entre Polyspace Bug Finder et Polyspace Code Prover

Polyspace^® Bug Finder™ et Polyspace Code Prover™ détectent les erreurs run-time par le biais d’une analyse statique. Même si les produits présentent une interface utilisateur similaire et que les mathématiques qui sous-tendent l'analyse sont parfois les mêmes, les objectifs des deux produits sont différents.

Bug Finder (ou Polyspace as You Code, qui effectue une analyse de fichier unique similaire à Bug Finder) analyse rapidement votre code et détecte de nombreux types de défauts. Code Prover vérifie chaque opération de votre code pour un ensemble d'erreurs run-time possibles et tente de prouver l'absence d'erreur pour tous les chemins d'exécution.

Remarque

Pour chaque opération de votre code, Code Prover examine tous les chemins d'exécution menant à l'opération qui n'ont pas entraîné d’erreur auparavant. Si un chemin d'exécution contient une erreur avant l'opération, Code Prover ne le prend pas en compte. Consultez Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).

Par exemple, pour chaque division de votre code, une analyse Code Prover tente de prouver que le dénominateur ne peut pas être zéro. Bug Finder ne procède pas à une telle vérification exhaustive. Par exemple, Bug Finder vérifie également l’éventuelle présence d’une erreur de division par zéro, mais il risque de ne pas trouver toutes les opérations susceptibles de causer l'erreur.

Les deux produits impliquent des différences dans la configuration, l'analyse et la revue des résultats, du fait de cette différence d'objectifs. Dans les sections suivantes, nous soulignons les principales différences qui distinguent une analyse Bug Finder d’une analyse Code Prover (également connue sous le nom de vérification). Selon vos besoins, vous pouvez intégrer l'un ou l'autre type d'analyse, ou les deux, à des moments appropriés dans le cycle de développement de votre logiciel.

Présentation des différences entre Bug Finder et Code Prover

Utilisez régulièrement à la fois Bug Finder et Code Prover dans votre processus de développement. Ces produits proposent un ensemble unique de fonctionnalités et se complètent l’un l’autre. Pour connaître les manières d’utiliser conjointement les deux produits, consultez Workflow avec à la fois Polyspace Bug Finder et Polyspace Code Prover.

Ce tableau présente la manière dont les deux produits se complètent. Pour de plus amples informations, consultez les sections ci-dessous.

Caractéristique	Bug Finder	Code Prover
Nombre de contrôleurs	+300 contrôleurs pour les défauts	30 vérifications pour les erreurs run-time critiques et 4 vérifications pour l'utilisation des variables globales
Profondeur d’analyse	Rapidité. Par exemple : Analyse plus rapide. Configuration et revue plus faciles. Moins d’exécutions pour obtenir un code propre. Résultats en temps réel.	Exhaustivité. Par exemple : Toutes les opérations d'un type donné sont vérifiées afin de détecter certaines erreurs critiques. Analyse plus rigoureuse des flux de données et de contrôle.
Critères de reporting	Défauts probables	Résultats avérés
Critères de recherche des bugs	Peu de faux positifs	Zéro faux négatif

Comment Bug Finder et Code Prover se complètent

• Analyse plus rapide avec Bug Finder

• Vérification plus exhaustive avec Code Prover

• Types de défauts plus spécifiques avec Bug Finder

• Processus de configuration plus simple avec Bug Finder

• Moins d’exécutions pour obtenir un code propre avec Bug Finder

• Résultats en temps réel avec Bug Finder

• Analyse plus rigoureuse des flux de données et de contrôle avec Code Prover

• Peu de faux positifs avec Bug Finder

• Zéro faux négatif avec Code Prover

• Règles de codage supportées dans Bug Finder

Analyse plus rapide avec Bug Finder

La rapidité de l'analyse Bug Finder dépend de la taille de l'application. Le temps d'analyse Bug Finder augmente proportionnellement à la taille de l'application. Le temps de vérification de Code Prover augmente à un rythme plus rapide que le temps linéaire.

Un workflow possible consiste à exécuter Code Prover pour analyser la robustesse des modules ou des bibliothèques par rapport à certaines erreurs et à exécuter Bug Finder au stade de l'intégration. L'analyse Bug Finder sur de grandes bases de code peut être effectuée dans un temps beaucoup plus court, et permet également de trouver des défauts d'intégration tels que Declaration mismatch et Data race.

Vérification plus exhaustive avec Code Prover

Code Prover tente de prouver l’absence des éléments suivants :

• Erreur Division by Zero à chaque opération de la division ou du module

• Erreur Out of Bounds Array Index à chaque accès au tableau

• Erreur Non-initialized Variable à chaque lecture de variable

• Erreur Overflow à chaque opération sujette à dépassement

etc.

Pour chaque opération :

• Si Code Prover réussit à prouver l'absence d'erreur pour tous les chemins d'exécution, il met l'opération en surbrillance verte.

• Si Code Prover réussit à prouver la présence d'une erreur définie pour tous les chemins d'exécution, il met l'opération en surbrillance rouge.

• Si Code Prover ne réussit pas à prouver l’absence d'erreur ou la présence d’une erreur définie, il met l'opération en surbrillance orange. Ces quelques vérifications orange soulignent les opérations que vous devez examiner attentivement, par le biais d'une inspection visuelle ou de tests. Les vérifications orange indiquent souvent la présence de vulnérabilités dissimulées. Par exemple, l'opération peut être sûre dans le contexte actuel mais échouer lorsqu'elle est réutilisée dans un autre contexte.

  Vous pouvez utiliser les informations fournies dans l'interface utilisateur Polyspace pour diagnostiquer les vérifications. Consultez Analyse plus rigoureuse des flux de données et de contrôle avec Code Prover. Vous pouvez également fournir des informations contextuelles pour réduire encore le code non prouvé, par exemple en limitant les plages d'entrée de manière externe.

Bug Finder n’a pas pour vocation de réaliser des analyses exhaustives. Il tente de détecter autant de bugs que possible et de réduire les faux positifs. En ce qui concerne les composants logiciels critiques, l'utilisation d'un outil de recherche de bugs n'est pas suffisante. En effet, malgré la correction de tous les défauts détectés lors de l'analyse, des erreurs peuvent persister lors de l'exécution du code (faux négatifs). Après avoir exécuté Code Prover sur votre code et résolu les problèmes détectés, vous pouvez vous attendre à ce que la qualité de votre code soit nettement supérieure. Consultez Zéro faux négatif avec Code Prover.

Types de défauts plus spécifiques avec Bug Finder

Code Prover vérifie les types d'erreurs run-time pour lesquels il est possible de prouver mathématiquement l'absence d'erreur. Outre la détection des erreurs dont l'absence peut être prouvée mathématiquement, Bug Finder détecte également d'autres défauts.

Par exemple, l'instruction if(a=b) est correcte d’un point de vue sémantique selon la norme du langage C, mais indique souvent une affectation involontaire. Bug Finder détecte ces opérations involontaires. Même si Code Prover ne détecte pas ces opérations involontaires, il peut détecter si une opération involontaire provoque d'autres erreurs run-time.

Parmi les exemples de défauts détectés par Bug Finder mais pas par Code Prover, citons les défauts de bonnes pratiques, les défauts de gestion des ressources, certains défauts de programmation, les défauts de sécurité et les défauts de design orientée objet en C++.

Pour plus d’informations, consultez :

• Défauts: Liste des défauts que Bug Finder peut détecter

• Run-Time Checks (Polyspace Code Prover): Liste des erreurs run-time que Code Prover peut détecter.

Processus de configuration plus simple avec Bug Finder

Même si la création de votre code réussit dans votre chaîne d'outils de compilation, elle peut échouer lors de la phase de compilation d'une vérification par Code Prover. La compilation stricte de Code Prover est liée à sa capacité à prouver l'absence de certaines erreurs run-time.

• À moins que vous n’utilisiez explicitement des options d'analyse qui émulent votre compilateur, Code Prover respecte strictement la norme ANSI^® C99.

  Pour autoriser des écarts par rapport à la norme ANSI C99, vous devez utiliser les options Cible et compilateur. Si vous créez un projet Polyspace à partir de votre système de création, les options sont définies automatiquement.

• Les erreurs de liaison admissibles dans les compilateurs courants ne le sont pas dans Code Prover.

  Même si votre compilateur autorise les erreurs de liaison telles que la non-concordance des signatures de fonctions d’une unité de compilation à l’autre, vous devez corriger ces erreurs afin d'éviter un comportement inattendu au run-time.

Pour plus d’informations, consultez Troubleshoot Compilation and Linking Errors (Polyspace Code Prover).

Bug Finder se montre moins strict quant à certaines erreurs de compilation. La présence d’erreurs de liaison, telles que la non-concordance des signatures de fonctions d’une unité de compilation à l’autre, peut interrompre une vérification Code Prover, mais pas une analyse Bug Finder. Par conséquent, vous pouvez exécuter une analyse Bug Finder en consacrant moins d’efforts à la configuration. Dans Bug Finder, les erreurs de liaison sont souvent signalées comme constituant un défaut une fois l’analyse terminée.

Moins d’exécutions pour obtenir un code propre avec Bug Finder

Pour garantir l'absence de certaines erreurs run-time, Code Prover respecte des règles strictes lorsqu'il détecte une erreur run-time dans une opération. Une fois qu'une erreur run-time s‘est produite, l'état de votre programme est défini comme étant incorrect et Code Prover ne peut pas prouver l'absence d'erreurs dans le code suivant. Par conséquent,

• Si Code Prover prouve la présence certaine d’une erreur et affiche une coche rouge, il ne vérifie pas le reste du code du même bloc.

  Les exceptions incluent notamment les vérifications telles que Overflow, pour lesquelles l'analyse se poursuit avec le résultat du dépassement tronqué ou remis à zéro (wrapped around).

• Si Code Prover suspecte la présence d'une erreur et affiche une coche orange, il ne prend pas en considération le chemin contenant l'erreur. Par exemple, si Code Prover détecte la présence d’une erreur Division by Zero dans l'opération 1/x, dans l'opération suivante qui concerne x dans ce bloc, x ne peut pas être zéro.

• Si Code Prover détecte qu'un bloc de code est inaccessible et affiche une coche grise, il ne détecte pas d'erreurs dans ce bloc.

Pour plus d’informations, consultez Code Prover Analysis Following Red and Orange Checks (Polyspace Code Prover).

Par conséquent, une fois que vous avez corrigé les coches rouges et grises et que vous relancez la vérification, vous pouvez repérer d'autres problèmes. Vous devez effectuer la vérification plusieurs fois et corriger les problèmes à chaque fois de manière à obtenir un code impeccable. La situation s’apparente aux tests dynamiques. Dans les tests dynamiques, une fois que vous avez corrigé une défaillance à un point donné du code, vous pouvez découvrir une nouvelle défaillance dans le code suivant.

Bug Finder n'interrompt pas l'analyse complète d'un bloc après y avoir détecté un défaut. Même avec Bug Finder, il se peut que vous deviez exécuter l'analyse plusieurs fois pour obtenir un code impeccable. Pour autant, le nombre d’exécutions nécessaire est inférieur par rapport à Code Prover.

Résultats en temps réel avec Bug Finder

Bug Finder affiche certains résultats alors que l’analyse est encore en cours. Nul n’est besoin d’attendre la fin de l’analyse pour examiner les résultats.

Code Prover n’affiche les résultats qu’une fois la vérification terminée. Lorsque Bug Finder détecte un défaut, il peut l’afficher. Code Prover doit prouver l’absence d’erreurs sur l’ensemble des chemins d’exécution. Par conséquent, il ne peut pas afficher de résultats pendant l’analyse.

Analyse plus rigoureuse des flux de données et de contrôle avec Code Prover

Pour chaque opération de votre code, Code Prover fournit :

• Info-bulles indiquant la plage de valeurs de chaque variable de l’opération.

  Dans le cas d’un pointeur, les info-bulles indiquent la variable vers laquelle le pointeur est dirigé, ainsi que les valeurs de la variable.

• Représentation graphique de la séquence d'appels de fonctions qui mène à l'opération.

Grâce à ces informations de plage et à ce graphique d'appels, vous pouvez facilement explorer la hiérarchie des appels de fonctions et comprendre la manière dont une variable acquiert les valeurs qui conduisent à une erreur. Par exemple, dans le cas d’une erreur Out of Bounds Array Index, vous pouvez trouver l'emplacement où la variable d'index se voit attribuer pour la première fois les valeurs qui conduisent à l'erreur.

Lorsque vous examinez un résultat dans Bug Finder, vous disposez également d'informations complémentaires pour comprendre la cause première d'un défaut. Par exemple, vous pouvez retracer l’historique d’un défaut détecté par Bug Finder jusqu'à sa cause première. Toutefois, Code Prover fournit des informations plus complètes, qui vous aideront à comprendre tous les chemins d'exécution de votre code.

Analyse du flux de données dans Code Prover

Analyse du flux de contrôle dans Code Prover

Peu de faux positifs avec Bug Finder

Bug Finder vise à ne donner que peu de faux positifs, autrement dit des résultats que vous n'êtes pas susceptible de corriger. Par défaut, seuls les défauts susceptibles d'être les plus significatifs pour vous sont affichés.

Bug Finder associe également un attribut appelé impact aux types de défauts en fonction de leur aspect critique et du taux de faux positifs. Vous pouvez choisir de ne rechercher que les défauts à fort impact lors de l'analyse de votre code. Vous pouvez également activer ou désactiver un défaut, selon que vous voulez ou non l’examiner.

De la même manière, vous pouvez désactiver dans Code Prover certains défauts liés à la non-initialisation.

Zéro faux négatif avec Code Prover

Code Prover vise à fournir une analyse exhaustive. Le logiciel vérifie chaque opération susceptible de déclencher certains types d’erreur. Si une opération de code apparaît en vert, cela signifie qu'elle ne peut pas provoquer d’erreurs run-time recherchées par le logiciel. Ainsi, le logiciel vise à signaler zéro faux négatif.

Le résultat Code Prover n'est valide que si vous exécutez votre code dans les mêmes conditions que celles que vous avez fournies à Code Prover par le biais des options d'analyse.

Si le logiciel ne réussit pas à prouver l'absence d'erreur, il met en surbrillance rouge ou orange l'opération suspecte et vous demande de l’examiner.

Règles de codage supportées dans Bug Finder

Bug Finder supporte la vérification de la conformité aux normes de codage externes, du type :

• AUTOSAR C++14. Consultez Règles AUTOSAR C++14.

• MISRA C:2012. Consultez Directives et règles MISRA C:2012.

• MISRA C++:2008. Consultez Règles MISRA C++:2008.

• CERT C. Consultez Règles et recommandations CERT C.

• CERT C Consultez Règles CERT C++.

Pour obtenir la liste complète des normes de codage supportées, consultez Polyspace Support for Coding Standards.

Voir aussi

Rubriques

• Workflow Using Both Polyspace Bug Finder and Polyspace Code Prover (Polyspace Code Prover)