Ours & Hippy — le blog [analyse_statique]

GuilOooo > Hum, ouais c’est l’idée d’annoter explicitement le langage C, une idée que j’affectionne pas mal, mais dont je n’ai jamais trouvé d’exécution satisfaisante (ÀMHA). Pour l’exemple, avec splint doit yavoir une annotation /*@null*/ si jme rappelle bien, mais ça remonte à loin mon dernier usage de splint. Sinon en Cyclone ya les pointeurs non nuls, ça doit être T @.

Mais à mon avis, la meilleure source d’informations ce sont les assertions. Je n’ai pas lu l’article mais à mon avis, ce devrait être la toute première source d’info. C’est traditionnel en C d’en placer à l’entrée des interfaces. Notamment, des choses comme assert(p != NULL) en entrée de fonction sont très fréquentes.

La méthode est expliquée après le premier code, et dans les commentaires. Ligne après ligne, des informations sont relevées, jusqu'à l'apparition d'une contradiction. C'est pas un algo particulièrement compliqué, mais c'est une idée qui leur a permis de trouver plein de bugs, contrairement à leurs autres méthodes.

Si j'ai bien compris ce que tu proposes, à mon avis le système de typage joue déjà ce rôle, ici on cherche d'autres bugs. Et oui, un typage évolué permet d'éviter plus de bugs, ce n'est pas une découverte. :)

Je comptais en premier lieu ne pas commenter jusqu'à avoir lu le papier. Me voici malgré tout, mais je commenterai sûrement à nouveau après l'avoir lu.

Une première remarque, cependant : on voit dans ton papier la méthode générale pour exploiter les informations données par le code source, mais pas la façon dont elles sont inférées. J'imagine que c'est dans le papier, mais c'est l'aspect qui m'intéresse le plus ici, donc je suis un peu resté sur ma faim.

Une question, ensuite : ne peut-on pas déléguer la récupération d'informations au système de type du langage ? Par exemple, on pourrait imaginer (même si le C est un mauvais exemple ici) deux types de pointeurs : le pointeur qui ne vaut jamais NULL, et celui qui peut valoir NULL. En C, c'est difficilement imaginable, mais dans un langage avec un système de type plus évolués, ce genre de choses est tout à fait réalisable : c'est en gros le type Maybe en Haskell (et son homologue en caml, dont j'ignore le nom).
Mon exemple se généralise-t-il bien aux autres techniques décrites dans la réaction, et le papier ?

gnomnain, ce sont des choses qui peuvent arriver. Le lock() peut avoir été fait dans une autre fonction. Au contraire je trouve ça intéressant pour deux raisons :

• on se demande si il y a un bug donc c’est peut-être pas une bonne pratique,
• le programme doit pouvoir aussi se débrouiller dans ces là. Il suppose que si on a appelé unlock() sans lock() avant, ça a été fait ailleurs (il préfère supposer que le programmeur sait ce qu’il fait, sinon il y aurait largement de quoi s’inquiéter en dehors des problèmes de concurrence).

Ce sont des questions traitées dans le papier que je vous encourage à lire si vous êtes intrigués.

Bien kiffant, surtout le dernier passage. Ça donne bien envie de lire la suite, sans nous laisser trop sur notre faim.

Par contre, par pitié, retire tes nom-prénom de la signature. Merci pour ta future engeance.

P.S. Sinon, c'est quoi ce délire avec les '☃' et '‽' ?

Ouais, moi aussi j'ai bien aimé l'article. Je me demandais juste si c'était normal qu'il y ait un unlock(lk) et pas de lock(lk) dans la fonction baz de l'exemple.

Article très intéressant parlant de techniques que je ne connaissais pas, merci :).

(I ♥ ☃)