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;
      }
    }
  }
}
  1. 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 tableau sieve?
  2. Même question en utilisant l’interface graphique (frama-c-gui -val exemple.c)
  3. Insérer des appels à la famille de fonctions built-in Frama_C_show_each_* pour étudier l’évolution des valeurs de i-2 et sieve[i-2] d’une part, i, j et sieve[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 par Frama_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.
  4. 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
  5. 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?
  6. 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
  7. Trouver un -slevel qui permet d’obtenir un singleton pour chacune des cases de sieve dans l’état final de l’analyse de valeur.
  8. 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++) {
  triangle[i][0] = 1;
  for (int j = 1; j<=i; j++) {
    triangle[i][j]=triangle[i-1][j] + triangle[i-1][j-1];
  }
 }
}

int main() {
  fill(MAX);
  return triangle[MAX][MAX/2];
}
  1. Lancer l’analyse de valeur sur la fonction main. Qu’observe-t-on?
  2. 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 de main?
  3. Avec le même -slevel que précédemment, relancer l’analyse avec l’option -lib-entry. Qu’observe-t-on?
  4. 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);
s=0;
for (k=0;k<N;k++){
s= s + *ptr_a * *ptr_b;
ptr_a++;
ptr_b += N;
}
*ptr_c=s;
}
}
}
  1. Que calcule cette fonction ?
  2. Le code se trouve dans le fichier pointers.c. Lancez frama-c et observeez les résultats (en particuliers ceux concernant les pointeurs).
  3. 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 ?
  4. 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

  1. Écrire une fonction main qui crée deux bstring à partir de chaînes C normales de 127 caractères ASCII quelconques, et en effectue la concaténation.
  2. Lancer l’analyse de valeur sur ce point d’entrée. Qu’observe-t-on.
  3. Écrire des wrapper pour malloc et realloc, en utilisant par exemple un tableau de char de taille SIZE_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é par malloc 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.
  4. Relancer l’analyse de valeur et vérifier si des erreurs à l’exécution sont possibles.
  5. 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

  1. Modifier la fonction ReadVertices pour créer un environnement de 25 points dont les coordonnées seront comprises entre -1000 et 1000
  2. 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.