Polyspace Code Prover
Prouvez l'absence d'erreurs run-time dans les logiciels
Polyspace Code Prover™ est un outil d'analyse statique permettant de prouver l'absence d'overflow, de division par zéro, de débordement de tableaux et autres erreurs run-time dans du code source C et C++. L'exécution du programme, l'instrumentation du code ou des cas de test ne sont pas nécessaires. Polyspace Code Prover utilise l'analyse sémantique et l'interprétation abstraite basée sur des méthodes formelles pour vérifier le comportement interprocédural, de contrôle et de flux de données du logiciel. Vous pouvez l'utiliser pour vérifier du code écrit à la main, du code généré ou une combinaison des deux types. Chaque instruction de code est repérée par un code couleur indiquant si elle est exempte de toute erreur run-time, avérée défaillante, inaccessible ou non prouvée.
Polyspace Code Prover affiche les informations de plage de valeur pour les variables et les valeurs retournées par les fonctions, et prouver quelles variables dépassent les limites de plage définies. Les résultats de vérification du code peuvent servir à effectuer le suivi des métriques de qualité et à vérifier la conformité à vos objectifs de qualité logicielle. Polyspace Code Prover peut être utilisé avec l'IDE Eclipse™ pour vérifier du code sur votre ordinateur de bureau.
Le support des normes industrielles est assuré par l’IEC Certification Kit (IEC 61508 et ISO 26262) et le DO Qualification Kit (DO-178).
En savoir plus :
Prouver l'absence d'erreurs run-time critiques
Identifiez les opérations de code C/C++ et Ada qui ne rencontreront aucune erreur run-time, quelles que soient les conditions d'exécution.
Détection des erreurs run-time
Détecter des erreurs impossibles à repérer avec d'autres méthodes de test
Analysez toutes les chemins du code par rapport à toutes les entrées possibles, sans exécuter le code.
Hiérarchie d'appels.
Créez des artefacts pour la certification
Réalisez le processus de certification du projet basés sur les normes de l'industrie.
DO Qualification Kit.
Comprenez la cause principale des problèmes et améliorez le design
Examinez le contrôle et le flux de données au sein du logiciel, et affichez les informations de plage associées à des variables et à des opérateurs.
Affichage par l'info-bulle des plages possibles pour toutes les conditions d'exécution.
Évitez les comportements logiciels indésirables
Trouvez toutes les sections de code qu'aucun chemin d'exécution ne permet d'atteindre, et identifiez les erreurs de logique et de structure du programme.
Identification du code mort.
Tracez les résultats de vérification du code jusqu'aux modèles Simulink
Vérifiez du code généré et assurez la traçabilité des résultats jusqu'au bloc source dans le modèle Simulink.
Traçabilité des résultats de vérification du code jusqu'au modèle Simulink.
Automatiser le processus de vérification du code
Utilisez Polyspace Code Prover Server™ pour exécuter le moteur d'analyse statique Polyspace Code Prover sur une machine de type serveur avec des outils d'automatisation intégrés, tels que Jenkins et Bamboo.
Automatiser le processus de vérification du code.
Notifiez et publiez les résultats pour une revue collaborative
Assignez automatiquement les défauts aux responsables des composants, envoyez des notifications par email et importez des résultats dans Polyspace Code Prover Access afin de trier et de résoudre les problèmes.
Envoyez des notifications par email avec les résultats de Polyspace Code Prover.
Examinez les résultats de Polyspace Code Prover afin de trier et de résoudre les problèmes
Polyspace Code Prover Access™ offre une interface web pour les résultats de vérification de code Polyspace et les métriques de qualité stockés dans une base de données centrale. Utilisez les outils de navigation dans votre navigateur web pour étudier les résultats de vérification du code, qui s'affichent à côté du code.
Détection des erreurs run-time
Objectifs de qualité des projets et du logiciel
Les tableaux de bord affichent des informations que vous pouvez utiliser afin de surveiller la qualité du logiciel, l'état des projets, le nombre de défauts, les métriques de code et les objectifs qualité du logiciel.
Tableau de bord de vue d'ensemble du projet.
S'intégrer avec les outils de suivi de bugs que vous utilisez déjà
Utilisez l'interface web afin de créer et d'assigner des tickets dans des outils de suivi de bugs comme Jira.
Création d'un ticket.
Support des compilateurs
définissez une analyse Polyspace pour émuler des compilateurs Microchip MPLAB XC16 et XC32
Vérification du code d’initialisation
vérifiez le code d’initialisation seul avant de vérifier le reste du programme et vérifiez si toutes les variables globales sont explicitement initialisées
Support de Simulink
analysez du code personnalisé appelé à partir des blocs C Function
Reportez-vous aux notes de version pour en savoir plus sur ces fonctionnalités et les fonctions correspondantes.
