Polyspace Code Prover

Affichage des informations sur les plages de valeur

Polyspace Code Prover suit le contrôle et le flux de données au sein du logiciel et affiche les informations de plage associées à des variables et à des opérateurs. En passant votre curseur sur un opérateur ou une variable, une info-bulle affiche les informations de plage. La méthode formelle appelée interprétation abstraite permet de déterminer des informations de plage précises afin de prouver que le logiciel est exempt de certaines erreurs d’exécution. Vous pouvez utiliser les informations de plage pour déboguer votre logiciel ou pour vous assurer que certaines variables ou opérations ne violent pas des limites de plage spécifiques.

Dans l’exemple ci-dessous, Polyspace Code Prover a établi que l’opération de division fait intervenir une plage de -1701 à 3276 pour l’opérande de gauche, tandis que l’opérande de droite vaut 9. Le résultat de la division est compris entre -189 et 364.

Tooltip displaying the possible ranges for all run time conditions.
Affichage par l’info-bulle des plages possibles pour toutes les conditions d’exécution.

Vous pouvez également visualiser le flux de contrôle à l’aide l’arbre d’appel et des graphiques du flux d’appel.

Call flow graph displaying the order of function calls in an interprocedural analysis.

Ordre des appels de fonction dans une analyse inter-procédures.

Point suivant: Suivi des métriques de qualité logicielle

Essayer Polyspace Code Prover

Obtenir une version d'évaluation

Automatiser et optimiser la vérification et le test de logiciel embarqué

Visionner le webinar