Polyspace pour la Vérification de Code C/C++

Jour 1 sur 3

Comparaison des outils Polyspace

Objectif: Se familiariser avec Polyspace Bug Finder et Polyspace Code Prover au travers d'un exemple.

• Workflows de vérification du code
• Exécution d'une analyse avec Polyspace Bug Finder
• Exécution d'une vérification avec Polyspace Code Prover
• Analyse et correction des défauts logiciels et des erreurs d՚exécution

Analyse avec Polyspace Bug Finder

Objectif: Vérifier du code qui ne respecte pas forcément la norme ANSI C en tenant compte de l'environnement d'exécution et corriger les défauts et les violations des règles de codage avec Polyspace Bug Finder.

• Création d'un projet Polyspace
• Artefacts usuels de l'environnement d'exécution
• Manipulation du code spécifique au processeur
• Réglage des options de configuration pour le hardware cible
• Analyse des défauts dans Polyspace Bug Finder
• Analyse des violations des règles MISRA C
• Mesure des métriques
• Partage des paramètres de configuration

Analyse des résultats de Polyspace Code Prover

Objectif: Savoir interpréter les résultats de Polyspace Code Prover.

• Notions d'interprétation abstraite
• Analyse de l'arbre d'appel
• Navigation dans le code source
• Interprétation des résultats de Polyspace Code Prover
• Visualisation des accès des variables globales dans le code source

Les checks de Polyspace Code Prover

Objectif: Comprendre les erreurs d'exécution à l'aide des informations de diagnostic disponibles dans Polyspace Code Prover.

• Vue d'ensemble des checks pour le code C
• Recherche des erreurs d'exécution avec Polyspace Code Prover
• Options utiles à la vérification
• Utiliser les espaces de travail

Jour 2 sur 3

Gestion des vérifications et des résultats de Polyspace Code Prover

Objectif: Gérer les résultats qui contiennent un grand nombre de checks non-prouvés.

• Workflows de vérification de Polyspace Code Prover
• Contrôle de la séquence d'exécution du programme
• Priorisation des erreurs potentielles d'exécution (orange)

Amélioration de la précision des vérifications de Polyspace Code Prover

Objectif: Apprendre comment Polyspace Code Prover gère le code manquant lors de la vérification, et comment modifier ce comportement pour produire des résultats plus significatifs.

• Vérification de robustesse et contextuelle
• Bouchonnage (stubbing) automatique
• Spécification de plage de données
• Bouchonnage (stubbing) manuel

Analyse avec Polyspace Access

Objectif: Découvrir comment gérer les résultats des vérifications lorsque la complexité du code augmente avec Polyspace Access™, et comment interpréter et comparer l'analyse d'intégration avec l'analyse de robustesse.

• Workflows post-soumission avec Polyspace Access
• Vérification contextuelle
• Détection des défauts d'intégration et des erreurs d'exécution

Analyse d'application

Objectif: Revoir la procédure et les options de configurations utiles pour vérifier une application complète.

• Problèmes logiciels d'une application
• Analyse des problèmes d'accès aux données partagées
• Remplacement des fonctions assembleur ou hardware
• Gestion de code tiers dans Polyspace
• Création de la documentation

Jour 3 sur 3

Atelier pratique (optionnel)

Objectif: Revoir les acquis de la formation et utiliser Polyspace directement sur un de vos projets. Parmi les sujets potentiels :

• Description des checks de Polyspace Bug Finder
• Vérification de code C++
• Analyse des tâches et des données partagées
• Vérification de code généré
• Revue du processus de développement
• Workflow d՚intégration
• Installation du logiciel en mode client/server
• Configuration de Polyspace
• Interprétation des résultats

Annexe F : Analyse d'intégration avec Polyspace Desktop

Objectif: Apprendre comment gérer les vérifications lorsque la complexité du code augmente, et comment interpréter et comparer l'analyse d'intégration avec l'analyse de robustesse.

• Vérification contextuelle
• Détection des défauts d'intégration et des erreurs d'exécution