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

Sécurité, vie privée... et Google Analytics!

 -  14 février - 

Ave, 'nal (ça fait vénal, je sait, c'est fait exprès). Il y a un détail qui m'intrigue: c'est très bien de vouloir la vie privée renforcée sur (...)


Suivre les amendements débattue à l'assemblée nationale avec Eliasse

 -  13 février - 

Il m'arrive parfois de suivre les séances de débats à l'assemblée nationale via la diffusion en direct ou en regardant les rediffusions vidéo. Le (...)


Utilisation de GtkTreeModel, GtkTreeView et consorts

 -  11 février - 

Sommaire Introduction Création du modèle et ajout des données Ajout d'un tri sur le modèle Ajout d'un filtre sur le modèle Affichage des données du (...)


Mettre en place des build automatiques avec jenkins et docker

 -  10 février - 

Sommaire Mettre en place des build automatiques avec jenkins et dockerOutils installation de docker installation de jenkins Création d'un agent (...)


Delta Chat est prêt pour le bureau

 -  7 février - 

Delta Chat est un logiciel de messagerie instantanée comme il en existe des milliers: on ajoute des contacts, on crée des groupes et s'envoie des (...)