Bon je n'ai pas beaucoup cherché, mais je n'ai pas réussi à faire marcher ça sur debian 8 (galère avec le changement d'abi des compilos, puis boost filesystem qui m'envoie chi… à l'exécution).
Je n'ai eu aucun problème sous Debian 8 personnellement. Regarde ce Dockerfile.
(Juste ça ne compile pas avec ninja ?!?)
En effet, je viens de voir ça. Étrange!
J'aurais aimé le passer sur le code du boulot, mais si j'ai bien compris, il n'y a pas de moyen d'analyser des bibliothèques dynamiques ?
Ou alors je n'ai pas trouvé comment passer un entry-point à scan-ikos ?
Malheureusement, on ne peut pas analyser de bibliothèques dynamiques avec ikos.
Par contre, tu peux créer un programme qui va appeler les fonctions de ta bibliothèque de façon arbitraire, et lancer ikos dessus.
En général, les projets utilisant IKOS en interne tournent sur un système d'exploitation temps réel.
En pratique, rien ne t'empêche d'utiliser IKOS pour un système sur bare metal. Dans ce cas, il te faudra probablement utiliser l'option --no-libc lors de l'analyse.
Ça donne quoi d'ailleurs si je le compile en mode "bibliothèque", puis je le lie à un autre code qui initialise la fonction à une autre implèm, comme le compilo a déjà choisi (suivant des règles invoquées depuis le Vide) bah mon implem je me la carre ?
Dans ton autre unité de compilation, tu ne peux pas modifier Do, vu qu'elle est marquée static. Sans toucher ce code, Do ne peut valoir que NULL ou EraseAll.
Do étant une variable globale, elle est déjà (implicitement) initialisée à zéro. Testez
static Function Do = nullptr;
Vous verrez que le comportement est le même.
D'après moi, il faudrait:
- Soit indiquer dans son type que ce pointeur ne dois jamais être null, ce qui forcerait l'utilisateur à donner une valeur par défaut. Mais ce n'est pas possible en C++..
- Soit utiliser un type optionnel (du genre std::optional) qui force l'utilisateur à traiter le cas où le pointeur est vide explicitement
Sinon, il faudrait déconseiller l'utilisation de pointeurs de fonction en C++. Au lieu de ça, on peut utiliser std::function.
Clang a tout à fait raison de produire ce code, comme expliqué ici.
Do est noté static, donc elle ne peut pas être modifiée directement par une autre unité de compilation.
La seule sémantique correcte pour ce programme est qu'une autre unité de compilation va appeler NeverCalled avant main, c'est donc ce que suppose Clang.
Le problème est dans le langage, pas dans l'implémentation.
À la limite, vous pouvez blâmer Clang de supposer que votre programme est correct..
On utilise cmake 2.8.12.2 au boulot, puisque c'est la version à peu prêt disponible partout (Red Hat, Debian 8, etc.), et aussi parce que c'est le minimum requis pour compiler nos dépendances (LLVM).
[^] # Re: Excellent !
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 1.
Je n'ai eu aucun problème sous Debian 8 personnellement. Regarde ce Dockerfile.
En effet, je viens de voir ça. Étrange!
Malheureusement, on ne peut pas analyser de bibliothèques dynamiques avec ikos.
Par contre, tu peux créer un programme qui va appeler les fonctions de ta bibliothèque de façon arbitraire, et lancer ikos dessus.
[^] # Re: Classique ?
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 1.
Quand je disais « classique », je pensais à cppcheck, clang-tidy et autre. C'est à dire, des analyseurs avec des heuristiques pour trouver des bugs.
C'est vrai que l'interprétation abstraite à 40 ans, mais en général quand je parle avec des ingénieurs, ils n'ont aucune idée de ce que c'est.
[^] # Re: Licence Nasa
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 1.
En effet, la NASA supporte aussi Apache.
En fait, ce projet a commencé en 2011 et a été publié à cette époque avec la licence NOSA, bien avant que j'arrive.
[^] # Re: Licence Nasa
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 3. Dernière modification le 17 décembre 2018 à 00:40.
C'est la licence de base pour les projets open source NASA. On ne m'a pas donné le choix.
[^] # Re: Vérification du code multi-threadé ?
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 3. Dernière modification le 15 décembre 2018 à 17:55.
Non, malheureusement on ne supporte pas le multi-thread.
[^] # Re: Une bonne nouvelle pour les fans de microcontrôleur ?
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 6. Dernière modification le 15 décembre 2018 à 01:11.
En général, les projets utilisant IKOS en interne tournent sur un système d'exploitation temps réel.
En pratique, rien ne t'empêche d'utiliser IKOS pour un système sur bare metal. Dans ce cas, il te faudra probablement utiliser l'option --no-libc lors de l'analyse.
[^] # Re: Ton journal est pertinent
Posté par Maxime Arthaud . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 5.
D'accord. J'aurais peut-être du ajouter quelques exemples.
[^] # Re: Erreur?
Posté par Maxime Arthaud . En réponse au journal Compilateur trop intelligent. Évalué à 2.
Dans ton autre unité de compilation, tu ne peux pas modifier
Do, vu qu'elle est marquéestatic. Sans toucher ce code,Done peut valoir que NULL ouEraseAll.[^] # Re: Comportement attendu
Posté par Maxime Arthaud . En réponse au journal Compilateur trop intelligent. Évalué à 4.
Doétant une variable globale, elle est déjà (implicitement) initialisée à zéro. Testezstatic Function Do = nullptr;Vous verrez que le comportement est le même.
D'après moi, il faudrait:
- Soit indiquer dans son type que ce pointeur ne dois jamais être null, ce qui forcerait l'utilisateur à donner une valeur par défaut. Mais ce n'est pas possible en C++..
- Soit utiliser un type optionnel (du genre
std::optional) qui force l'utilisateur à traiter le cas où le pointeur est vide explicitementSinon, il faudrait déconseiller l'utilisation de pointeurs de fonction en C++. Au lieu de ça, on peut utiliser
std::function.# Comportement attendu
Posté par Maxime Arthaud . En réponse au journal Compilateur trop intelligent. Évalué à 2.
Clang a tout à fait raison de produire ce code, comme expliqué ici.
Do est noté
static, donc elle ne peut pas être modifiée directement par une autre unité de compilation.La seule sémantique correcte pour ce programme est qu'une autre unité de compilation va appeler
NeverCalledavantmain, c'est donc ce que suppose Clang.Le problème est dans le langage, pas dans l'implémentation.
À la limite, vous pouvez blâmer Clang de supposer que votre programme est correct..
[^] # Re: Existe-t-il des compilateurs C/C++ qui donnent une sémantique à tous les programmes ?
Posté par Maxime Arthaud . En réponse au journal Compilateur trop intelligent. Évalué à 2.
Je préfère:
# CMake 2.8.12.2
Posté par Maxime Arthaud . En réponse au journal Version minimum de CMake. Évalué à 1.
On utilise cmake 2.8.12.2 au boulot, puisque c'est la version à peu prêt disponible partout (Red Hat, Debian 8, etc.), et aussi parce que c'est le minimum requis pour compiler nos dépendances (LLVM).
Un peu de
cmake_policy(), et ça roule.[^] # Re: Vidéos
Posté par Maxime Arthaud . En réponse à la dépêche Capitole du Libre 2013 - le programme. Évalué à 2.
TVn7, le club vidéo de l'ENSEEIHT, filme les conférences, et elles seront mise en ligne après, sur le site du capitole du libre.