Analyse Statique de Programmes – TP Frama-C
ENSIIE 3ème année – année scolaire 2015/2016 Enseignants: Tristan Le Gall et Virgile Prevosto
5 janvier 2016
Exercice 1: Crible
On considère le programme suivant, dont le code est dans exemple.c:
#define MAX 128
int sieve[MAX];
int main() {
for (int i = 2; i <= MAX+1; i++) {
if (sieve[i-2]==0) {
for(int j = i - 2; j < MAX; j+=i) {
sieve[j] = i;
}
}
} }
- Lancer l’analyse de valeur sur ce programme, à l’aide de la commande
frama-c -val exemple.c
. Qu’observe-t-on pour les valeurs possibles des éléments du tableausieve
? - Même question en utilisant l’interface graphique (
frama-c-gui -val exemple.c
) - Insérer des appels à la famille de fonctions built-in
Frama_C_show_each_*
pour étudier l’évolution des valeurs dei-2
etsieve[i-2]
d’une part,i
,j
etsieve[j]
d’autre part lors du calcul du point fixe pour les boucles externe et interne respectivement. On rappelle qu’une fonction dont le nom commence parFrama_C_show_each_
peut prendre un nombre arbitraire d’arguments, dont l’évaluation dans l’état courant de l’analyse de valeur sera affiché sur la sortie standard chaque fois que l’analyse atteint ce point. - Une première possibilité d’amélioration des résultats consiste à utiliser l’option
-wlevel
, qui modifie le moment où le widening se déclenche. Observer ce qui se passe si on utilise-wlevel 10
- Une seconde possibilité consiste à dérouler syntaxiquement certaines boucles. Pour cela, on utilise l’annotation
/*@ loop pragma UNROLL n; */
oùn
est un entier au-dessus de la boucle qu’on veut dérouler. Dérouler 50 fois la boucle externe et 25 fois la boucle interne. Qu’observe-t-on? - La méthode privilégiée d’amélioration des résultats de l’analyse de valeur est l’option
-slevel
qui autorise l’analyse à propager un certain nombre d’états distincts par instruction avant de faire l’union. Qu’obtient-on comme résultat avec-slevel 200
- Trouver un
-slevel
qui permet d’obtenir un singleton pour chacune des cases desieve
dans l’état final de l’analyse de valeur. - Que calcule ce programme?
Exercice 2: Triangle de Pascal
On considère le programme suivant, dont le code est dans pascal.c:
#define MAX 21
int triangle[MAX][MAX];
void fill(int n) {
if (n <= 0 || n > MAX) return;
for (int i =0; i < n; i++) {
0] = 1;
triangle[i][for (int j = 1; j<=i; j++) {
1][j] + triangle[i-1][j-1];
triangle[i][j]=triangle[i-
}
}
}
int main() {
fill(MAX);return triangle[MAX][MAX/2];
}
- Lancer l’analyse de valeur sur la fonction
main
. Qu’observe-t-on? - Après avoir éventuellement corrigé le programme pour faire disparaitre l’erreur, relancer l’analyse de valeur en augmentant la précision via
-slevel
. Quelle est la valeur de retour demain
? - Avec le même
-slevel
que précédemment, relancer l’analyse avec l’option-lib-entry
. Qu’observe-t-on? - Corriger éventuellement le programme pour qu’il renvoie la même réponse qu’à la question 2 y compris en utilisant
-lib-entry
Exercice 3: Arithmetique de pointeurs
On considère des matrices carrée de taille N, encodées dans des tableau de longueur NxN. (Cf pointers.c)
void m_func (int N, int a[], int b[], int c[]) {
int i=0,j=0,k=0,s=0;
int *ptr_a,*ptr_b,*ptr_c;
for (i=0;i<N;i++){
for (j=0;j<N;j++){
ptr_a = a+ (i*N);
ptr_b = b+ j;
ptr_c = c+ (i*N + j);0;
s=for (k=0;k<N;k++){
s= s + *ptr_a * *ptr_b;
ptr_a++;
ptr_b += N;
}
*ptr_c=s;
}
} }
- Que calcule cette fonction ?
- Le code se trouve dans le fichier pointers.c. Lancez frama-c et observeez les résultats (en particuliers ceux concernant les pointeurs).
- Est-il possible qu’à la fin du programme, les pointeurs ne soient pas initalisés ? Si non, comment améliorer la précision de l’analyse ?
- Que dit l’analyse sur les valeurs de la matrice c en sortie ? Que se passe-t-il si on augmente la précision via
-slevel
ou-wlevel
? Quelle autre option envisager pour améliorer la précision ?
Exercice 4: Chaînes de caractères
On s’intéresse à la bibliothèque bstring, qui fournit une représentation alternative des chaînes de caractères. Le code est disponible sur le site et dans cette archive
- Écrire une fonction
main
qui crée deuxbstring
à partir de chaînes C normales de 127 caractères ASCII quelconques, et en effectue la concaténation. - Lancer l’analyse de valeur sur ce point d’entrée. Qu’observe-t-on.
- Écrire des wrapper pour
malloc
etrealloc
, en utilisant par exemple un tableau dechar
de tailleSIZE_MAX
et un tableau auxiliaire destiné à stocker à chaque indice de base d’un bloc alloué la taille du bloc correspondant. On ne cherchera pas à vérifier qu’un accès dans un bloc alloué parmalloc
ne déborde pas dans un autre bloc, ni si on accède au bloc après sa libération.free
peut donc ne rien faire. - Relancer l’analyse de valeur et vérifier si des erreurs à l’exécution sont possibles.
- Adapter la fonction
main
pour concaténer deux chaînes de longueur au plus 63
Exercice 5: Triangulation
On considère une implantation d’un algorithme de triangulation du plan donné dans le livre Computational Geometry in C de J. O’Rourke, et disponible ici
- Modifier la fonction
ReadVertices
pour créer un environnement de 25 points dont les coordonnées seront comprises entre-1000
et1000
- Lancer l’analyse de valeur sur le programme et vérifier l’absence d’erreur à l’exécution. On pourra reprendre l’implantation de
malloc
de l’exercice précédent.