Polyspace Code Prover

Détection des erreurs d’exécution

Polyspace Code Prover utilise l’interprétation abstraite avec l’analyse statique de code afin de prouver, d’identifier et de diagnostiquer des erreurs d’exécution telles que les dépassements (overflows), les divisions par zéro et les débordements pointeur. Cette technique vérifie complètement et intégralement toutes les conditions d’exécution et fournit automatiquement un diagnostic de preuve, d’échec, d’inaccessibilité ou d’absence de preuve pour chaque opération de code. Dans les résultats de vérification produits par Polyspace Code Prover, chaque opération C ou C++ est repérée par un code couleur indiquant son statut :

Vert: fiabilité prouvée, sans aucune erreur d’exécution
Rouge: erreur prouvée chaque fois que l’opération est exécutée
Gris: inaccessibilité prouvée / code mort (peut indiquer un problème fonctionnel)
Orange: opération non prouvée pouvant présenter une erreur sous certaines conditions

Color-coded run-time error attributes identified by Polyspace Code Prover.

Attributs d’une erreur d’exécution identifiée par Polyspace Code Prover.

Les erreurs détectées comprennent :

  • Overflows, underflows, divisions par zéro et autres erreurs arithmétiques
  • Débordements de tableau et pointeurs déréférencés illégalement
  • Conditions toujours vraies / fausses
  • Membres de classe non initialisées (C++)
  • Accès en lecture à des données non initialisées
  • Accès un pointeur null this (C++)
  • Code mort
  • Erreurs dynamiques liées à la programmation objet, à l’héritage et à la gestion des exceptions (C++)
Point suivant: Affichage des plages de valeur

Essayer Polyspace Code Prover

Obtenir une version d'évaluation

Automatiser et optimiser la vérification et le test de logiciel embarqué

Visionner le webinar