Salut à tous,

Laissez moi vous présenter IKOS: https://github.com/NASA-SW-VnV/ikos

IKOS est un analyseur statique pour C et C++ basé sur LLVM, développé à la NASA. Il est gratuit et open source.

IKOS permet de détecter des bugs dans vos programmes C et C++. Contrairement à un analyseur statique « classique », il se repose sur une théorie mathématique appelée [Interprétation Abstraite](https://fr.wikipedia.org/wiki/Interpr%C3%A9tation_abstraite). IKOS prouve automatiquement l’inexistence de bugs dans vos programmes, pour toutes les exécutions possibles. En contrepartie, IKOS peut générer des faux positifs, dans les cas où le code n'a pas pu être prouvé correct par l'analyse. IKOS est similaire à Polyspace, Astrée ou Frama-C (analyse de valeur).

IKOS peut détecter la plupart des bugs en C, tels que les débordements de tampon, les divisions par zéro, etc. La liste complète (en anglais) est disponible [ici](https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#checks). Cette liste est globalement similaire à la liste des checks d'UBSan. IKOS peut aussi être utilisé pour prouver une condition arbitraire, en utilisant __ikos_assert(condition).

IKOS a été conçu pour analyser des codes de systèmes embarqués écrit en C, et c'est la qu'il est le plus efficace.

Pour tout problème, n'hésitez pas à ouvrir un rapport de bug sur Github (en anglais si possible). Nous apprécions aussi les retours par email: ikos@lists.nasa.gov