Découverte de Frama-C, l'un des outils incontournables d'analyse de code en C

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
97
Mois de parution
juillet 2018
Domaines


Résumé
Malgré son nom, Frama-C n'est pas un énième clone libre d'une solution reconnue éditée par Framasoft. Il s'agit d'un framework d'analyse et de preuve de code C, doté d'une interface graphique facilitant son utilisation. Cet article permettra de se familiariser avec cet outil pour que vous vous assuriez que vos programmes font bien ce que vous attendez d'eux.

On peut considérer qu'un programme « fonctionne » lorsqu'il répond aux exigences fixées par les développeurs. Toutefois ces exigences peuvent être plus ou moins strictes : s'agit-il seulement d'avoir un programme qui ne crashe pas ou d'assurer que pour toute donnée bien formée qui lui est transmise, le programme retourne bien le résultat attendu ? C'est la notion de preuve informatique que nous touchons du doigt : contrairement aux tests qui ne portent nécessairement que sur des points précis, la preuve est complète, elle tient compte de tous les cas possibles. Nous n'allons pas rentrer dans le domaine théorique de la preuve informatique, domaine fort intéressant, mais qu'il serait vain de tenter de couvrir en quelques pages. Dans cet article, nous nous contenterons d'aborder un aspect pratique des preuves avec le framework Frama-C (FRAmework for Modular Analysis of C code).

1. Présentation et installation

Frama-C est développé par le CEA LIST (Software Security...

Cet article est réservé aux abonnés. Il vous reste 92% à découvrir.
à partir de 21,65€ HT/mois/lecteur pour un accès 5 lecteurs à toute la plateforme
J'en profite


Articles qui pourraient vous intéresser...

Persistance et objets en C++

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
114
Mois de parution
mai 2021
Domaines
Résumé

Au travers de deux articles [1-2] sur les principes de l’orienté objet en C++, nous avions abordé encapsulation, héritage, et polymorphisme. Nous proposons dans ce nouvel article les classes de base pour gérer la persistance d’objets dans des fichiers. Ces classes utilisent les principes énoncés ci-dessus et présentent des stratégies via la généricité. Un exemple de stratégie pour stocker en binaire pourra être redéfini pour d’autres stratégies, comme un stockage en XML.

Principes de l’orienté objet en C++ : la généricité

Magazine
Marque
GNU/Linux Magazine
Numéro
248
Mois de parution
mai 2021
Domaines
Résumé

La programmation orientée objet obéit à des principes. Les 4 principaux sont l’encapsulation, l’héritage, le polymorphisme et la généricité. Dans un premier article, nous avons évoqué l’encapsulation, puis l’héritage et le polymorphisme dans un deuxième. Ce troisième et dernier article traite de la généricité.

Flutter : applications mobiles, web et desktop

Magazine
Marque
GNU/Linux Magazine
Numéro
248
Mois de parution
mai 2021
Domaines
Résumé

Flutter est un framework permettant de développer des applications natives pour Linux, Windows, macOS, Android, iOS et le Web à partir du même code source. Un moteur graphique OpenGL ultra performant et la compilation native en ARM, x86-64 ainsi que WebAssembly, associés à un cycle de développement agile et hyper intuitif, en font la solution ultime pour les créateurs d’applications. L’essayer, c’est l’adopter !

Un bot qui surveille le Web et envoie des alertes

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
114
Mois de parution
mai 2021
Domaines
Résumé

De nos jours, lorsque l’on recherche une information, on se tourne immédiatement vers le Web. Ainsi, de très nombreuses informations sont mises à jour quotidiennement et il faut donc penser à visiter les sites les produisant, de manière à être au courant des dernières modifications. Et si nous codions un bot qui ferait cela pour nous ?