Polyspace Client for Ada

Prouver l'absence d'erreurs run-time dans le code source

Polyspace Client™ for Ada prouve l’absence d’overflow, de division par zéro, de dépassement de tableaux et de certaines autres erreurs run-time dans le code source Ada83 et Ada95. Il produit des résultats sans nécessité d'exécution du programme, d’instrumentation du code ou de cas de tests. Polyspace Client for Ada utilise des techniques d’interprétation abstraite reposant sur des méthodes formelles pour valider le code. Les résultats de l’analyse sont affichés dans le code source. Un code couleur est utilisé pour indiquer si chaque instruction dans le code est exempte d’erreurs run-time, avérée défaillante, inaccessible ou non prouvée. Polyspace Client for Ada affiche les informations de plage pour les variables et les valeurs renvoyés par les fonctions ; il peut identifier les variables qui dépassent les limites de plage spécifiées.

Vous pouvez utiliser Polyspace Client for Ada sur votre ordinateur pour exécuter des analyses de code et les passer en revue avant la compilation et les tests.

Polyspace Client for Ada utilise plusieurs couleurs pour identifier les instructions Ada qui ont été vérifiées de manière statique.

Prouver l’absence d’erreurs run-time critiques

Vérifiez que les opérations run-time du code Ada83 ou Ada95 sont correctes. Identifiez les instructions qui ne généreront jamais d’erreur run-time, quelles que soient les conditions du run-time. Analysez les vulnérabilités run-time identifiées avec le support du suivi des événements, des plages de valeur de variable et des arbres d'appels. Polyspace Client for Ada utilise des méthodes formelles pour détecter des erreurs qui échappent aux autres types de test. Analysez tous les chemins du code avec toutes les entrées possibles sans exécuter le code.

CSEE Transport assure la fiabilité du logiciel pour les trains à grande vitesse

Documentation

Trois fenêtres sont ouvertes. Une avec des instructions utilisant un code couleur, une avec des paramètres et une avec des éléments graphiques.

Analyse interactive sur desktop

Organisez et configurez vos projets, et exécutez une analyse de code statique sur un sous-ensemble de projets logiciels pour qualifier les changements de code avant de les soumettre sur le dépôt principal du code source. Utilisez Polyspace Client for Ada pour générer des rapports, puis consulter et trier les résultats. Identifiez les causes principales des bugs complexes grâce aux vues debug permettant de naviguer pas à pas dans chaque instruction qui conduit à une erreur run-time.

Documentation

Polyspace Client for Ada vous permet d'obtenir la liste de toutes les variables globales du logiciel analysé.

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

Examinez les flux de contrôle et de données dans le logiciel, et consultez les informations sur les plages associées aux variables et aux opérateurs.

NATO HAWK Management Office accélère l’analyse des applications critiques

Documentation

Polyspace Client for Ada affiche le code inaccessible en gris dans le code source.

Optimiser le logiciel pour de meilleures performances

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

Documentation

Polyspace Client for Ada permet d'afficher un graphique du chemin conduisant à une possible situation d'accès concurrent aux données.

Analyser l’utilisation des variables globales

Réduisez le temps consacré au débuggage des opérations de lecture/écriture sur des variables globales, notamment les variables communes à plusieurs tâches ou threads. Identifiez les flux de contrôle et de données conduisant à une situation d'accès concurrent aux données, avec le graphe des accès concurrents. Identifiez les variables globales inutilisées pour optimiser le code.

Documentation

Test statique de sécurité des applications

Prouvez que l’application est exempte de vulnérabilités critiques de sécurité en testant exhaustivement les instructions ADA potentiellement vulnérables telles que les accès à la mémoire, les dépassements de mémoire tampon ou les dépassements numériques. 20 règles de vulnérabilité CWE sont supportées. Exploitez les résultats d'analyse de Polyspace Server for Ada pour compléter ou remplacer le fuzzing et vous concentrer sur les opérations sources de vulnérabilités.

Sécurité embarquée avec l'analyse statique Polyspace (1:52)

Polyspace Client for Ada calcule toute la hiérarchie des appels pour les applications Ada.

Améliorer et compléter les tests de robustesse et les tests fonctionnels

Utilisez Polyspace Client for Ada pour améliorer les tests de robustesse en vous concentrant sur les instructions dangereuses telles que la division par zéro ou les overflows. Exploitez les résultats de Polyspace Server for Ada pour créer et gérer les tests de limites et de partition, tout en tirant parti des analyses des flux de contrôle et de données, ainsi que des plages calculées pour les paramètres des fonctions et les variables globales.

EADS assure la fiabilité des lanceurs spatiaux

Documentation