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

Débugage facile avec Sentry

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
111
Mois de parution
novembre 2020
Domaines
Résumé

Nous le savons tous, aucun code n’est exempt de bugs. Nous avons beau écrire tous les tests unitaires du monde, tous les tests fonctionnels, avoir une couverture du code par nos tests de 200 %, il y a toujours des bugs qui passent à travers les mailles du filet. Sentry est là pour vous aider à les trouver et à les corriger grâce à vos utilisateurs, et ce, sans qu’ils ne s’en rendent compte.

Résolution azimutale d’un RADAR à bruit : analyse et réalisation d’un RADAR à synthèse d’ouverture (SAR) par radio logicielle

Magazine
Marque
GNU/Linux Magazine
Numéro
242
Mois de parution
novembre 2020
Domaines
Résumé

Nous complétons la mesure de distance des cibles RADAR par la mesure d’azimut rendue possible par la synthèse d’ouverture d’antenne, afin de localiser leur position et ainsi d’identifier précisément leur nature par superposition sur une photographie aérienne. La souplesse de la radio logicielle est illustrée par la montée en fréquence (2,4 GHz), sans modifier aucun élément matériel autre que les antennes.

Débogage JavaScript côté client

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
111
Mois de parution
novembre 2020
Domaines
Résumé

Si JavaScript a longtemps évoqué l’idée de petit script dans un site internet, il est aujourd’hui souvent utilisé comme fondation d’application web complexe (notamment via des frameworks comme ReactJS ou VueJS). Dans ce contexte d’usage avancé, il est nécessaire d’avoir en main les bons outils et techniques de débogage.

Principes de l’orienté objet en C++ : l’encapsulation

Magazine
Marque
GNU/Linux Magazine
Numéro
242
Mois de parution
novembre 2020
Domaines
Résumé

La programmation orientée objet obéit à des principes. Les 4 principaux principes sont l’encapsulation, l’héritage, le polymorphisme et la généricité. Que de noms barbares, que nous allons démystifier de manière logique ! Des exemples déclinés dans le langage C++ illustreront ces principes. Ce premier article traite de l’encapsulation.

Déboguer un exécutable Java

Magazine
Marque
GNU/Linux Magazine
HS n°
Numéro
111
Mois de parution
novembre 2020
Domaines
Résumé

On attribue souvent au succès de Java la relative simplicité de sa syntaxe et surtout son vaste écosystème. C’est oublier un point essentiel dans son adoption : son débogueur et ses fonctionnalités qui simplifient tant le travail d’analyse et de résolution d’une erreur à l’exécution.