bonjour,
et merci pour ce billet !
Je me permets d'apporter des précisions sur le comportement de certains outils statiques, puisque tu as écris que tu n'as pas eu l'occasion d'en tester à part clang analyzer.
Je peux te détailler ce que trouve l'outil Polyspace puisque je fais partie de l'équipe !
Un outil comme Polyspace Code Prover va chercher à prouver si l'assert est toujours vrai ou toujours faux à partir de ce qu'il sait du code, en propageant l'ensemble des valeurs possibles par exemple (c'est plus complexe que ça).
Et en fait il fait cette preuve pour toutes les opérations du code, pas seulement les asserts.
Pour ce qui est de ton exemple, Code Prover est tout d'abord suffisamment précis pour calculer la valeur de std::sin(0), r est donc égal à 0.0.
L'assert de la post-condition est donc prouvé comme toujours vrai (ce qui se traduit par une couleur verte dans Polyspace). Ça c'est le premier point.
A la sortie de sin(0), dans main(), la valeur -1.0 sera donc propagée à sqrt. Cette fois l'assert sera prouvé toujours faux (couleur rouge) puisque n vaut -1.0.
Maintenant que se passe-t'il si dans sin, au lieu d'une valeur connue, on affecte une valeur random entre 0.0 et disons 5.0 à r:
const double r = static_cast <float> (rand()) / (static_cast <float> (RAND_MAX/5.0));
Ici Code Prover ne pourra pas prouver si l'assert de post-condition est vrai ou faux, et le signalera par une couleur orange, indiquant au passage qu'il y a quelque chose à regarder à cet endroit. Ça tombe bien c'est justement le but des post-conditions.
De plus il continuera en considérant que r est dans l'intervalle de l'assert.
A la sortie de sin, r sera donc entre 0.0 et 1.0 et donc dans sqrt() n sera entre -1.0 et 0.0. Et par conséquent on aura aussi un assert orange pour la pré-condition.
Partager