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

Jour 1 sur 3

Présentation de la méthode de travail avec 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 résolution de problème software

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 informations sur le hardware cible
• Analyse des défauts dans Polyspace Bug Finder
• Analyse des violations des règles MISRA C
• Mesure des métriques
• Projets modèles

Analyse des Résultats de Polyspace Code Prover

Objectif: Devenir compétent dans l'interprétation des résultats 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 de l'utilisation des variables globales dans le code source

Points de contrôle de la vérification de code

Objectif: Trouver les erreurs d'exécution à l'aide des diagnostics 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

Jour 2 sur 3

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

Objectif: Gestion des résultats de vérification qui contiennent un grand nombre de point de contrôle non-prouvés.

• Workflows des vérifications de Polyspace Code Prover
• Contrôle de la séquence d'exécution du programme
• Priorisation dans la recherche des erreurs d'exécution orange

Ajout de précision aux 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 automatique
• Spécification de plage de données
• Bouchonnage manuel

Analyse d'intégration avec Polyspace Access

Objectif: Découvrir comment gérer les résultats de vérification 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 utiles pour vérifier une application complète.

• Problèmes relatifs au software d'une application
• Analyse des problèmes d'accès aux données partagées
• Remplacement des fonctions d'assemblage 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 de données partagées entre tâches
• Vérification de code généré
• Revue du processus de développement
• Intégration du workflow
• Installation du logiciel 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
• Création de nouveaux modules
• Détection des défauts d'intégration et des erreurs d'exécution