SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231
SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232
ENSIIE 3ème année - année 2010/2011
Enseignants : Virgile Prevosto et Julien Signoles
14 janvier 2011
Le but de ce TP est d'utiliser l'outil Frama-C et en particulier son greffon d'analyse de valeur. La version installée à l'ENSIIE est Beryllium-20090902.
Frama-C est fondé sur un ensemble de greffons proposant chacun un type d'analyse
particulier. La liste des greffons disponibles peut être obtenue par
frama-c -help
. De même, les options permettant de piloter le noyau
s'obtiennent avec frama-c -kernel-help
. Nous nous intéresserons en
particulier aux options -main
, -lib-entry
et -pp-annot
.
De plus, nous utiliserons avant tout le greffon value
, fondé sur
l'interprétation abstraite (cf. cours précédent). Ses options sont accessibles
par frama-c -value-help
. Les options les plus importantes pour ce TP sont
-val
, -slevel
et -wlevel
.
Enfin, il existe une interface graphique, frama-c-gui
, qui accepte les
mêmes options que frama-c
.
On considère l'implantation de la factorielle telle que vue dans le cours 3: (fichier fact.c)
int fact(int x) { int y = 1; int z = 1L; while (y <= x) { z = z * y; y++; } return z; }
On utilise l'option -main fact
pour indiquer que le point d'entrée de
notre analyse est la fonction fact
, et l'option -val
pour lancer
l'analyse de valeur. Qu'indique Frama-C pour les valeurs possibles de x
,
y
et z
?
On va maintenant analyser fact
dans un contexte particulier: on
s'intéresse au cas où x
est compris entre 0 et 100. Pour cela, on peut
écrire une fonction qui va assigner à x
une valeur présentant les bonnes
propriétés puis appeler fact
(fichier fact_context.c):
#include "fact.c" volatile int entropy; int interval(int min, int max) { int res = entropy; if (res < min) res = min; if (res > max) res = max; return res; } int main (void) { int x = interval(0,100); return fact(x); }
La fonction interval
renvoie un de ses deux arguments en fonction d'une
valeur inconnue et qui change à chaque appel.
main
. Quelles sont les valeurs calculées pour x
, y
et z
?-wlevel
pour retarder le moment où Frama-C fait un élargissement. Quelle est la valeur minimale pour laquelle on obtient la meilleure précision possible sur y
?-slevel
qui propage des états séparés jusqu'à un certain point.z
? Donner la plus grande valeur possible pour x
qui ne fait pas apparaître le problème.
On peut aussi guider l'analyse de valeur par des annotations ACSL: Avec un
slevel
approprié, une disjonction conduira à une analyse sur deux états
séparés. On considère le programme suivant (fichier annot.c):
int x, y, z; void f(int c) { int* p = 0; if (c == 1) p = &x; if (c == 2) p = &y; if (c == 3) p = &z; if (0<c && c <4) *p=42; }
f
, considéré comme un appel de bibliothèque (option -lib-entry
, qui a pour effet de ne pas considérer que dans l'état du début d'analyse les variables globales sont initialisées à 0
(ou NULL
, ou 0.0
suivant le type de données).-slevel
? Pourquoi?slevel
minimal qui permet de faire une analyse sans warning?
Une implantation possible de la fonction memcpy
de la bibliothèque
standard du C est la suivante (fichier memcpy.c):
void *memcpy(void *src, void* dst, int size) { unsigned long dst_val = ((unsigned long) dst) % 4 ; int todo = size; char *dstc = (char *) dst; char *srcc = (char *) src; for (int i=0; i < dst_val && todo > 0; i++) { *dstc++ = *srcc++; todo--; } int *dsti = (int *) dstc; int *srci = (int *) srcc; while (todo>=4) { *dstc++=*srci++; todo-=4; } dstc=(char*)dsti; srcc=(char*)srci; for (int i=0; i < todo; i++) { *dstc++=*srci++; } return dst; }
On effectue la copie par blocs de 4 caractères, excepté éventuellement au début (pour faire des écritures alignées en mémoire) ou à la fin (s'il reste moins de 4 caractères à copier).
n
de caractères arbitraire entre 0 et 512 entre deux buffers distincts ne provoque pas d'accès hors-borne, et qu'après un appel à memcpy
les n
premières cases de dst
ont été initialisées.dst_val
, Frama-C ne gérant pas bien les modulo sur des valeurs issues de pointeurs.
On s'intéresse maintenant à des fonctions sur des chaînes de caractères C,
c'est à dire des blocs d' unsigned char
comportant un élément égal à
0
.
strlen
qui étant donné une chaîne retourne le premier index pointant sur 0
.strlen
ne fait pas d'accès hors-borne pour toute chaîne de longueur inférieure ou égale à 63 caractères (0
final exclu), et utiliser l'analyse de valeur pour vérifier qu'aucun warning n'apparaît.strcpy
, qui copie le contenu de son premier argument dans le deuxième, pour des chaînes de taille au plus 63. Pour le contexte, on considérera deux cas: tout d'abord celui où la source et la destination sont deux buffers distincts, puis celui où source et destination sont deux parties du même bloc mémoire (avec un recouvrement potentiel).