Greboca  

LinuxFr.org : les journaux  -  IKOS, un analyseur statique développé à la NASA

 -  Décembre 2018 - 

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. 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. 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

Commentaires : voir le flux atom ouvrir dans le navigateur

par Maxime Arthaud

LinuxFr.org : les journaux

LinuxFr.org : Journaux

PHP 7.3 apporte le support des contrôles dans PHP-LDAP

 -  19 janvier - 

Sommaire PHP-LDAP PHP 7.2: les opérations étendues PHP 7.3: les contrôles Futur PHP 7.3 est sorti le 6 décembre 2018 et apporte le support des (...)


Hackathon Factur-X le 24-25 janvier 2019 à Paris

 -  19 janvier - 

Le Forum National de la Facture Electronique (FNFE-MPE) organise un Hackathon sur Factur-X le 24-25 janvier 2019 dans les locaux de GS1 France à (...)


Debian, installations automatiques et ARM

 -  16 janvier - 

Sommaire Installation réseau automatisée pour x86mauvais sujet, changer sujet on cause d'ARM?ARM, boot standard ARM, boot réseau Conclusion et purge (...)


Mes activités open-sources / libres récentes

 -  10 janvier - 

Sommaire ExchangeCalendar Home Bank acme-dns-tiny xmpp-pane et Ibex Hein ? Kadabra évolue ! Cher journal, Toujours dans l'idée de parler des (...)


Sur l'intérêt des systèmes de protections des courriers électroniques (DKIM, SPF et DMARC)

 -  7 janvier - 

Sommaire SPF, DKIM, et DMARCSPF : Sender Policy Framework DKIM : DomainKeys Identified Mail DMARC : Domain Message Authentication Reporting & (...)