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

Une nouvelle interface graphique pour WBO

 -  24 juin - 

Il y quelques temps, j'ai évoqué ici WBO, un logiciel libre de dessin collaboratif en ligne (dépêche). Le logiciel a bien évolué depuis l'annonce (...)


Les 10 ans d'Hadopi

 -  13 juin - 

Pour les 10 ans de la Hadopi et ses psychodrames de cacahuètes, môssieur Marc Rees, rédacteur en chef de la revue en ligne Next Inpact, a concocté (...)


Moi, expert C++, j'abandonne le C++

 -  3 juin - 

Sommaire Ma passion C++11, C++14, C++17… Comprendre le client et développer vite Intégrer l’utilisateur final dans son équipe Faire des sprints d’une (...)


Huawei renié par Google : une bonne nouvelle pour les smartphones libres (ou pas) ?

 -  21 mai - 

La nouvelle est parue ce matin : https://www.theverge.com/2019/5/19/18631558/google-huawei-android-suspension En gros, Google coupe l’accès aux (...)


Qualcomm corrige une faille critique dans des dizaines de puces Snapdragon

 -  8 mai - 

Pour continuer sur les discussions autour d'Android du moment sur LinuxFR. Source : https://app.beebom.com/qualcomm-patches-critical-flaw-dozens-snap