Polyspace Code Prover

Prouver l'absence d'erreurs run-time dans un logiciel

Polyspace Code Prover™ prouve l'absence d'overflow, de division par zéro, de dépassement de tableaux et de certaines autres erreurs run-time dans du code source C et C++. Il produit des résultats sans nécessité d'exécution du programme, d’instrumentation du code ou de cas de tests. Polyspace Code Prover utilise l'analyse statique et des techniques d'interprétation abstraite reposant sur des méthodes formelles. Vous pouvez l'utiliser sur du code manuel, du code généré, ou une combinaison des deux. Un code couleur est utilisé pour indiquer si chaque opération est exempte d’erreurs run-time, avérée défaillante, inaccessible ou non prouvée.

Polyspace Code Prover affiche également les informations de plage pour les variables et les valeurs renvoyées par les fonctions ; il peut identifier les variables qui dépassent les limites de plage spécifiées. Les résultats peuvent être publiés dans un tableau de bord pour permettre le suivi des métriques de qualité et garantir la conformité avec les objectifs de qualité logicielle.

Le support des normes industrielles est assuré via l'IEC Certification Kit (for IEC 61508 and ISO 26262) et le DO Qualification Kit (for DO-178).

Introduction à Polyspace Code Prover

Utilisation des résultats d'analyse du code et des couleurs du code source.

Prouver l’absence d’erreurs run-time critiques

Analysez tous les chemins du code avec toutes les entrées possibles sans exécuter le code. Identifiez les instructions qui ne seront jamais associées à une erreur run-time, quelles que soient les conditions run-time, et trouvez d'autres instructions nécessitant votre intervention.

Documentation

Affichage d'une info-bulle montrant les plages possibles pour les conditions run-time.

Améliorer le design du logiciel et la compréhension du code

Examinez les flux de contrôle et de données dans votre code C/C++, et consultez les informations sur les plages associées aux variables et aux opérateurs.

Documentation

Détecter le code mort dans la logique et la structure du programme.

Optimiser le logiciel pour de meilleures performances

Supprimez le code défensif en identifiant les opérations sûres et sécurisées, telles que la division par zéro et les overflows. Détectez les branches du code qui ne sont accessibles par aucun chemin d'exécution. Trouvez les erreurs dans la logique et la structure du programme, et supprimez-les pour réduire l'empreinte mémoire.

Documentation

Volet d'affichage d'accès aux variables.

Analyser l’utilisation des variables globales

Passez moins de temps à débugger les opérations de lecture/écriture sur des variables globales, comme les variables partagées par plusieurs tâches ou plusieurs threads.
Utilisez le graphe des accès concurrents pour comprendre les flux de contrôle et de données susceptibles de conduire à des situations d'accès concurrent aux données. Identifiez les variables globales inutilisées pour optimiser le code.

Documentation

Support de certification

Créez les artefacts nécessaires pour finaliser le processus de certification aux normes industrielles. Certification réalisée par TÜV SÜD pour une utilisation avec les normes IEC 61508 et ISO 26262. Utilisez les rapports et les artefacts pour les processus DO-178C.

Documentation

Intégration de Simulink et Stateflow

Exécutez une analyse sur le code généré et tracez vos résultats jusqu'aux blocs sources du modèle Simulink^® et aux graphiques Stateflow^®. Démarrez une analyse Polyspace^® directement depuis l'environnement Simulink.

Documentation

Analyse interactive sur desktop

Exécutez une analyse statique de code sur des projets logiciels complets ou des sous-ensembles. Utilisez l'outil desktop pour générer des rapports, puis examinez et triez les résultats.
Identifiez la cause première de bugs complexes en mode debug, en naviguant pas à pas dans chaque instruction qui conduit à une erreur run-time. Organisez et configurez vos projets, avec le support natif de plus de 60 compilateurs C et C++, et la configuration automatique de l'analyse Polyspace extraite du système de compilation du projet.

Documentation

Test statique de sécurité des applications

Prouvez l'absence de vulnérabilités de sécurité critiques telles que les dépassements de mémoire tampon, l'accès à la mémoire et les dépassements numériques. Réduisez la nécessité du fuzzing en analysant le code sur l'ensemble des chemins du code et des entrées sans exécuter le code.