préparation TP

config/cert_exp_33.c

+void set_flag(int number, int *sign_flag) {
+  if (NULL == sign_flag) {
+    return;
+  }
+
+  if (number > 0) {
+    *sign_flag = 1;
+  } else if (number < 0) {
+    *sign_flag = -1;
+  }
+}
+
+int is_negative(int number) {
+  int sign;
+  set_flag(number, &sign);
+  return sign < 0;
+}

config/cert_exp_33_realloc.c

+#include <stdlib.h>
+#include <stdio.h>
+enum { OLD_SIZE = 10, NEW_SIZE = 20 };
+
+int *resize_array(int *array, size_t count) {
+  if (0 == count) {
+    return 0;
+  }
+
+  int *ret = (int *)realloc(array, count * sizeof(int));
+  if (!ret) {
+    free(array);
+    return 0;
+  }
+
+  return ret;
+}
+
+void func(void) {
+
+  int *array = (int *)malloc(OLD_SIZE * sizeof(int));
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < OLD_SIZE; ++i) {
+    array[i] = i;
+  }
+
+  array = resize_array(array, NEW_SIZE);
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < NEW_SIZE; ++i) {
+    printf("%d ", array[i]);
+  }
+}

config/cwe20.c

+#include <stdio.h>
+#include <stdlib.h>
+void die(const char* s) {
+    printf("%s",s);
+    exit(2);
+}
+
+#define MAX_DIM 15
+
+typedef int board_square_t;
+
+/* board dimensions */
+
+int main () {
+    int m,n, error;
+    board_square_t *board;
+    printf("Please specify the board height: \n");
+    error = scanf("%d", &m);
+    if ( EOF == error ){
+    die("No integer passed: Die evil hacker!\n");
+    }
+    printf("Please specify the board width: \n");
+    error = scanf("%d", &n);
+    if ( EOF == error ){
+    die("No integer passed: Die evil hacker!\n");
+    }
+    if ( m > MAX_DIM || n > MAX_DIM ) {
+    die("Value too large: Die evil hacker!\n");
+    }
+    board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+    for (int i = 0; i < m; i++) {
+        for (int j = 0; j < n; j++) {
+            board[n*i+j] = 0;
+        }
+    }
+    if (board[(m-1)*n] == 0) return 0; else return 1;
+}

config/example1.c

+// example1.c - Demonstrates miniz.c's compress() and uncompress() functions (same as zlib's).
+// Public domain, May 15 2011, Rich Geldreich, richgel99@gmail.com. See "unlicense" statement at the end of tinfl.c.
+#include <stdio.h>
+#include "miniz.h"
+typedef unsigned char uint8;
+typedef unsigned short uint16;
+typedef unsigned int uint;
+
+// The string to compress.
+static const char *s_pStr = "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson." \
+  "Good morning Dr. Chandra. This is Hal. I am ready for my first lesson.";
+
+int main(int argc, char *argv[])
+{
+  uint step = 0;
+  int cmp_status;
+  uLong src_len = (uLong)strlen(s_pStr);
+  uLong cmp_len = compressBound(src_len);
+  uLong uncomp_len = src_len;
+  uint8 *pCmp, *pUncomp;
+  uint total_succeeded = 0;
+  (void)argc, (void)argv;
+
+  printf("miniz.c version: %s\n", MZ_VERSION);
+
+    // Allocate buffers to hold compressed and uncompressed data.
+    pCmp = (mz_uint8 *)malloc((size_t)cmp_len);
+    pUncomp = (mz_uint8 *)malloc((size_t)src_len);
+    if ((!pCmp) || (!pUncomp))
+    {
+      printf("Out of memory!\n");
+      return EXIT_FAILURE;
+    }
+
+    // Compress the string.
+    cmp_status = compress(pCmp, &cmp_len, (const unsigned char *)s_pStr, src_len);
+    if (cmp_status != Z_OK)
+    {
+      printf("compress() failed!\n");
+      free(pCmp);
+      free(pUncomp);
+      return EXIT_FAILURE;
+    }
+#ifdef DECOMPRESS
+  // Decompress.
+  cmp_status = uncompress(pUncomp, &uncomp_len, pCmp, cmp_len);
+  if (cmp_status != Z_OK)
+    {
+      printf("uncompress() failed!\n");
+      free(pCmp);
+      free(pUncomp);
+      return EXIT_FAILURE;
+    }
+#endif
+  printf("Success.\n");
+  return EXIT_SUCCESS;
+}

config/libstring.c

+#include <string.h>
+#include <stdlib.h>
+#include <ctype.h>
+#include <assert.h>
+#include <unistd.h>
+#include <stdbool.h>
+
+
+#define unlikely(x)    __builtin_expect(!!(x), 0)
+
+#include "libstring.h"
+
+#define BUF_LEN 65536
+#define CAP_DEFAULT 10
+
+
+string_t *string_colored(const char *str, enum stringcolor c) {
+  int n =  strlen(str) + strlen(COLOR_DEFAULT) + strlen(COLOR_BLACK);
+  string_t *s = malloc(sizeof(string_t) + n);
+  if(unlikely(s == NULL)) return NULL;
+  s->len = n;
+  switch(c) {
+  case BLACK:   memcpy(s->buf,COLOR_BLACK,strlen(COLOR_BLACK));     break;
+  case RED:     memcpy(s->buf,COLOR_RED,strlen(COLOR_RED));         break;
+  case GREEN:   memcpy(s->buf,COLOR_GREEN,strlen(COLOR_GREEN));     break;
+  case YELLOW:  memcpy(s->buf,COLOR_YELLOW,strlen(COLOR_YELLOW));   break;
+  case BLUE:    memcpy(s->buf,COLOR_BLUE,strlen(COLOR_BLUE));       break;
+  case MAGENTA: memcpy(s->buf,COLOR_MAGENTA,strlen(COLOR_MAGENTA)); break;
+  case CYAN:    memcpy(s->buf,COLOR_CYAN,strlen(COLOR_MAGENTA));    break;
+  case WHITE:   memcpy(s->buf,COLOR_WHITE,strlen(COLOR_WHITE));     break;
+  default: break;
+  }
+  memcpy(&(s->buf[strlen(COLOR_BLACK)]), str, strlen(str));
+  n -=  strlen(COLOR_DEFAULT);
+  memcpy(&(s->buf[n]), COLOR_DEFAULT, strlen(COLOR_DEFAULT));
+  return s;
+}
+
+/**********************************************************************/
+
+string_t *string_nnew(const char *str, size_t len) {
+  string_t *s = malloc(sizeof(string_t) + len);
+  if(unlikely(s == NULL)) return NULL;
+  s->len = len;
+  memcpy(s->buf, str, len);
+  return s;
+}
+
+/**********************************************************************/
+
+string_t *string_new(const char *str) {
+  return string_nnew(str, strlen(str));
+}
+
+/**********************************************************************/
+
+string_t *string_clone(const string_t *str) {
+  return string_nnew(str->buf, str->len);
+}
+
+/**********************************************************************/
+
+string_t *string_readfd(int fd) {
+  char buf[BUF_LEN];
+  int n = read(fd ,buf, BUF_LEN-1);
+  if(unlikely(n<0) ) return string_new("");
+  buf[n] = '\0';
+  return string_new(buf);
+}
+
+/**********************************************************************/
+
+string_t *string_readline(FILE *stream) {
+  char buf[BUF_LEN];
+  if(!fgets(buf, BUF_LEN-1, stream)) return string_new("");
+  buf[strlen(buf)-1] = '\0';
+  return string_new(buf);
+}
+
+
+/**********************************************************************/
+
+string_t *string_concat(const string_t *s1, const string_t *s2) {
+  string_t *s = malloc(sizeof(string_t) + s1->len + s2->len);
+  if(unlikely(s == NULL)) return NULL;
+  s->len = s1->len + s2->len;
+  memcpy(s->buf, s1->buf, s1->len);
+  memcpy(s->buf+s1->len, s2->buf, s2->len);
+  return s;
+}
+
+/**********************************************************************/
+
+string_t *string_trim(const string_t *str) {
+  size_t l=0;
+  int r= str->len-1;
+  while(l < str->len && isspace(str->buf[l])) l+=1;
+  while(r>=0 && isspace(str->buf[r])) r-=1;
+  r+=1;
+  
+  if( unlikely(l> (size_t) r)) return string_new("");
+
+  return string_nnew( &(str->buf[l]), r-l);
+}
+
+/**********************************************************************/
+
+string_t *string_map(charfunc_t fun, const string_t *str) {
+  string_t *s = string_clone(str);
+  if(unlikely(s == NULL)) return NULL;
+  for(size_t i=0;i<s->len;i++) {
+    s->buf[i] = fun(s->buf[i]);
+  }
+  return s;                             
+}
+
+/**********************************************************************/
+
+string_t *string_filter(boolfunc_t fun, const string_t *str) {
+  int c=0;
+  char *tmp = malloc(str->len);
+  memcpy(tmp,str->buf,str->len);
+  for(size_t i=0; i < str->len; i++)
+    if(fun(str->buf[i])) tmp[c++] = str->buf[i]; 
+  tmp[c] = '\0';
+  string_t *s = string_new(tmp);
+  free(tmp);
+  return s;                             
+}
+
+/**********************************************************************/
+
+int string_compare(const string_t *s1,const string_t *s2) {
+  int n = (s1->len < s2->len) ? s1->len : s2->len;
+  int r = strncmp(s1->buf, s2->buf, n);
+
+  return r ? r : (int)(s1->len - s2->len);
+}
+
+/**********************************************************************/
+
+bool string_equal(const string_t *s1, const string_t *s2) {
+  if(s1->len != s2->len) return false;
+  return strncmp(s1->buf,s2->buf,s1->len) == 0 ? true : false;   
+}
+
+/**********************************************************************/
+
+string_t *string_substring(const string_t *str, size_t start, size_t end){
+  if(unlikely(!(start <= end) && (end <= str->len))) return NULL;
+
+  return string_nnew(&(str->buf[start]), end-start);
+}
+
+/**********************************************************************/
+
+string_t *string_repeat(const string_t *str, size_t times) {
+  size_t n =  str->len * times;
+  if( unlikely(!n)) return string_new("");
+  
+  string_t *s = malloc(sizeof(string_t) + n);
+  if( unlikely(!s)) return NULL;
+  
+  s->len = n;
+  for(size_t i=0; i < times; i++)
+    memcpy(&(s->buf[i*(str->len)]), str->buf, str->len);
+  
+  return s;
+}
+
+/**********************************************************************/
+
+
+char *string_tocstr(const string_t *str) {
+  char *cstr = malloc(str->len +1);
+  if( unlikely(cstr==NULL)) return NULL;
+  memcpy(cstr, str->buf, str->len);
+  cstr[str->len] = '\0';
+  return cstr;
+}
+
+/**********************************************************************/
+
+static int string_substring_index_offset(const string_t *str, const string_t *substring, size_t offset) {
+  if(unlikely(substring->len == 0)) return offset;
+  if(unlikely(substring->len > (str->len - offset) )) return -1;
+
+  for(size_t i=offset; i<= str->len - substring->len; i++) {
+    for(size_t j=0; j < substring->len; j++) {
+      if(str->buf[i+j] != substring->buf[j]) break;
+      if( (j+1) == substring->len) return i;
+    }
+  }
+  return -1;
+}
+
+
+int string_substring_index(const string_t *str, const string_t *substring) {
+  return string_substring_index_offset(str,substring, 0);
+}
+
+
+/**********************************************************************/
+
+bool string_is_substring(const string_t *str, const string_t *sub, size_t off) {
+  if(unlikely(sub->len+off > str->len)) return false;
+  if(unlikely(sub->len == 0)) return true;
+  return strncmp(&(str->buf[off]), sub->buf, sub->len) ? false : true;
+  
+}
+
+
+
+/**********************************************************************/
+
+string_t *string_replace_char(const string_t *str, char old, char new) {
+  string_t *s =  string_clone(str);
+
+  for(size_t i=0; i < s->len; i++) 
+    s->buf[i] = (s->buf[i] == old) ? new : s->buf[i];
+
+  return s;
+}
+
+
+/**********************************************************************/
+
+/*
+ * Implementation of the string_replace() function is based on the
+ * suggestion by OpenAI's GPT-3.5
+ */
+
+string_t *string_replace(const string_t *str, const string_t *old, const string_t *new) {
+  size_t n = 0;
+  int offset = 0;
+  
+  while( (offset = string_substring_index_offset(str, old, offset)) > -1  ) {
+    offset+=old->len;
+    n += 1;
+  }
+  
+  if(n==0) return string_clone(str);
+  size_t len =  str->len + n * (new->len - old->len);
+  string_t *s = malloc(sizeof(string_t) + len);
+  s->len = len;  
+  
+  char *t = s->buf;
+  int curr = 0;
+  offset=0;
+  while(n--) {
+    offset = string_substring_index_offset(str, old, offset);
+    memcpy(t, str->buf+curr, offset-curr);
+    t += offset-curr;
+
+    memcpy(t, new->buf, new->len);
+    t += new->len;
+    curr = offset + old->len;
+    offset+=old->len;
+  }
+  memcpy(t, str->buf+curr, str->len-curr);
+  
+  
+  return s;
+}
+  
+
+
+/**********************************************************************/
+
+string_vector_t *string_split(const string_t *str, char delimiter) {
+  string_vector_t *svec = string_vector_empty();
+  size_t start = 0;
+  for(size_t i=0; i< string_len(str); i++)
+    if(str->buf[i]==delimiter) {
+      string_vector_add(svec, string_nnew(&(str->buf[start]), i-start));
+      start = i+1;
+    }
+  string_vector_add(svec, string_nnew(&(str->buf[start]), string_len(str)-start));
+  return svec;
+}
+
+
+/**********************************************************************/
+
+string_vector_t *string_ssplit(const string_t *str, string_t *delimiter) {
+  string_vector_t *svec = string_vector_empty();
+  int idx = string_substring_index(str, delimiter);
+  if(idx==-1) {
+    string_vector_add(svec, string_clone(str));
+    return svec;
+  }
+  string_vector_add(svec, string_nnew(str->buf, idx));
+  idx += string_len(delimiter);  
+  
+  for(size_t i=idx; i<= string_len(str)-string_len(delimiter); i++) {
+    for(size_t j=0; str->buf[i+j] == delimiter->buf[j]; j++)
+      if( (j+1) == delimiter->len-1) {
+        string_vector_add(svec, string_nnew(&(str->buf[idx]), i-idx));
+        idx = i + string_len(delimiter);
+        i += string_len(delimiter);  
+        break;
+      }
+  }
+  if( (size_t) idx <= string_len(str))
+    string_vector_add(svec, string_nnew(&(str->buf[idx]), string_len(str)-idx));
+    
+  return svec;
+}
+
+
+/*************************************************************************
+ *                           String Vector                               *
+ *************************************************************************/
+
+string_vector_t *string_vector_empty() {
+  string_vector_t *svec = malloc(sizeof(string_vector_t));
+  if(unlikely(svec==NULL)) return NULL;
+  svec->buf = malloc(CAP_DEFAULT * sizeof(string_t *));
+  svec->cap = CAP_DEFAULT;
+  svec->top = -1;
+  return svec;
+}
+
+string_vector_t *string_vector_new(string_t *str) {
+  string_vector_t *svec = string_vector_empty();
+  if(unlikely(svec==NULL)) return NULL;
+  string_vector_add(svec, str);
+  return svec;
+}
+  
+bool string_vector_is_empty(const string_vector_t *svec) {
+    return svec->top == -1;
+}
+
+
+void string_vector_free(string_vector_t *svec) {
+  free(svec->buf);
+  free(svec);
+}
+
+void string_vector_deepfree(string_vector_t *svec){
+  for(int i=0;i <= svec->top; i++) free(svec->buf[i]);
+  string_vector_free(svec);
+}
+
+bool string_vector_is_full(string_vector_t *svec) {
+    return (size_t) (svec->top + 1) == svec->cap; 
+}
+
+void string_vector_resize(string_vector_t *svec) {
+  svec->buf = realloc(svec->buf, 2 * svec->cap * sizeof(string_t *));
+  svec->cap *= 2;
+}
+
+int string_vector_find(const string_vector_t *svec, const string_t *str) {
+  for(int i= 0; i<=svec->top; i++) 
+    if (string_equal(svec->buf[i] , str)) return i;
+  return -1;
+}
+
+void string_vector_add(string_vector_t *svec,  string_t *str) {
+  if (string_vector_is_full(svec)) string_vector_resize(svec);
+  svec->top += 1;
+  svec->buf[svec->top] = str;
+}
+
+
+/**********************************************************************/
+
+
+string_t *string_vector_remove(string_vector_t *svec, size_t index) {
+  if ((int)index > svec->top) return NULL;
+  string_t *str = svec->buf[index];
+  for(int i=index; i<svec->top; i++) svec->buf[i] = svec->buf[i+1];
+  svec->top -=1;
+  return str;
+}
+
+
+/**********************************************************************/
+
+bool string_vector_equal(const string_vector_t *a, const string_vector_t *b) {
+  if(a->top != b->top) return false;
+  for(int i=0;i<=a->top;i++) if(!string_equal(a->buf[i],b->buf[i])) return false;
+  return true;   
+}
+
+/**********************************************************************/
+
+string_vector_t *string_vector_map(strfunc_t func,
+                                   const string_vector_t *svec) {
+  if(string_vector_len(svec) == 0)  return string_vector_empty();
+
+  string_vector_t *res = malloc(sizeof(string_vector_t));
+  if(unlikely(!res)) return NULL;
+  res->buf = malloc(svec->cap * sizeof(string_t *));
+  res->cap = svec->cap;
+  res->top = svec->top;
+  memcpy(res->buf, svec->buf, svec->top * sizeof(string_t *));
+  
+  for(int i = 0; i<= svec->top; i++) res->buf[i] = func(svec->buf[i]);
+
+  return res;
+}
+
+/**********************************************************************/
+
+string_vector_t *string_vector_filter(strboolfunc_t func,
+                                      const string_vector_t *svec) {
+  string_vector_t *res = string_vector_empty();
+  if(unlikely(!res)) return NULL;
+  for(int i = 0; i<= svec->top; i++)
+    if(func(svec->buf[i])) string_vector_add(res, string_clone(svec->buf[i])); 
+  
+  return res;     
+}
+
+/**********************************************************************/
+
+string_t *string_vector_reduce(reducefunc_t func,
+                               const string_vector_t *svec,
+                               string_t *initializer) {
+  string_t *val = (initializer) ? string_clone(initializer) : string_new("");
+  
+  for(int i = 0; i<= svec->top; i++) {
+    string_t *t = func(val,svec->buf[i]);
+    free(val);
+    val = t;
+  }
+  return val;
+}
+
+
+/**********************************************************************/
+
+
+const char *libstring_version() {
+  return LIBSTRING_VERSION;
+}

tp.md

+# Analyse Statique de Programmes -- TP Frama-C
+
+CentraleSupélec
+
+Enseignant: Virgile Prevosto
+
+## Préliminaires
+
+Une image docker est disponible ici: https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl
+et peut être utilisée soit localement, soit depuis `MyDocker`. Les fichiers C utilisés pour ce TP sont tous dans le répertoire
+`config`, qui est monté automatiquement dans le container docker si vous utilisez les scripts associé ([PowerShell](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.ps1) pour Windows ou [sh](https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl/blob/main/start-3asl.sh) pour Linux/macOS/BSD). Ces scripts devraient automatiquement ouvrir un onglet de votre navigateur web avec une session IceWM. Si ce n'est pas le cas, vous pouvez le faire manuellement: http://localhost:3000
+
+L'image Docker contient Frama-C 29.0, ce que l'on peut vérifier en lançant `frama-c -version` dans un shell.
+
+Dans ce TP, nous allons essentiellement utiliser le greffon Eva. Lancer l'analyse se fait en passant l'option `-eva` à
+Frama-C. L'ensemble des options du greffon peut se retrouver avec
+`frama-c -eva-help`. Le manuel du greffon est également disponible sur
+[le site de Frama-C](https://frama-c.com/download/eva-manual-29.0-Copper.pdf). Notez toutefois que les options nécessaires pour réaliser le TP seront
+mentionnées dans l'énoncé.
+
+## CERT C EXP33-C. Do not read uninitialized memory
+
+On s'intéresse dans cet exercice à un exemple tiré des [règles de codage C du CERT](https://wiki.sei.cmu.edu/confluence/display/c/SEI+CERT+C+Coding+Standard) américain. En l'occurrence, il s'agit d'illustrer la règle [EXP33-C](https://wiki.sei.cmu.edu/confluence/display/c/EXP33-C.+Do+not+read+uninitialized+memory), qui rappelle qu'il est important de s'assurer que toute location mémoire dans laquelle on lit a été préalablement initialisée.
+
+L'exemple est reproduit ci-dessous, et se trouve également dans le fichier [`cert_exp_33.c`](config/cert_exp_33.c).
+
+```c
+#include <stddef.h>
+
+void set_flag(int number, int *sign_flag) {
+  if (NULL == sign_flag) {
+    return;
+  }
+
+  if (number > 0) {
+    *sign_flag = 1;
+  } else if (number < 0) {
+    *sign_flag = -1;
+  }
+}
+
+int is_negative(int number) {
+  int sign;
+  set_flag(number, &sign);
+  return sign < 0;
+}
+```
+
+### Première exécution de Frama-C
+
+Le fragment de code fourni n'est pas une application complète. Il va donc falloir indiquer à Frama-C quel est le point d'entrée de notre analyse.
+Lancer `frama-c -eva -main is_negative cert_exp_33.c`. Quels sont les messages émis? Lequel correspond au problème évoqué sur le site du CERT?
+
+Lancer ensuite l'interface graphique: `frama-c-gui -eva -main is_negative cert_exp_33.c`, et remarquer l'assertion ACSL générée par Eva au dessus de l'instruction contenant potentiellement un comportement indéfini. Regarder également l'onglet `Red Alarms`, qui indique s'il existe des alarmes se produisant à coup sûr pour au moins un état abstrait (mais pas nécéssairement pour tous les états atteignant le même point de programme). Vérifier qu'il n'y a pas de telle alarme.
+
+Utiliser l'onglet `Values` de l'interface graphique pour déterminer la valeur d'expressions en différents points du programme en cliquant sur les expressions en question comme sur l'exemple ci-dessous pour `number` dans le deuxième `if` de `set_flag`:
+![interface graphique de Frama-C/Eva](frama-c-gui.png)
+
+Dans la suite du TP, on proposera préférentiellement d'utiliser l'interface textuelle, mais il est toujours possible d'utiliser les mêmes options avec l'interface graphique. Le contenu affiché sur le terminal dans le premier cas se trouve alors dans l'onglet `Console` de l'interface graphique.
+
+### Afficher des valeurs en cours d'analyse
+
+L'alarme levée par Eva n'est que potentielle: on ne sait pas quelles valeurs de `number` pourrait y conduire, ni même s'il ne s'agit pas en fait d'une _fausse alarme_. Pour aller un peu plus loin, nous allons demander à Eva d'effectuer une analyse plus précise. Tout d'abord, afin de mieux voir comment s'effectue la propagation des valeurs abstraites, nous allons ajouter des appels à des fonctions `Frama_C_show_each_*`: chaque fois qu'Eva atteint un de ces appels, l'analyseur affichera la valeur abstraite calculée pour chacun des arguments fournis.
+
+Ajouter l'instruction `Frama_C_show_each_set_flag(number, *sign_flag);` à la fin de la fonction `set_flag`, et `Frama_C_show_each_is_negative(number, sign);` après l'appel à `set_flag` dans `is_negative`, puis lancer `frama-c` avec les mêmes arguments que précédemment et observer l'affichage obtenu.
+
+### Partitionner les traces
+
+Un des moyens d'améliorer la précision de l'analyse consiste à utiliser le _partitionnement de traces_, c'est à dire à ne pas systématiquement fusionner les états abstraits provenant de différentes branches, mais à propager simultanément plusieurs états abstraits, suivant certains critères. Eva propose notamment l'option `-eva-partition-history`, qui prend un entier `n` en argument. Lorsque cette option est activée, les traces qui diffèrent sur au moins 1 des `n` dernières conditions rencontrées seront gardées séparées.
+
+Lancer Eva en ajoutant cette option, pour différentes valeurs de `n`. Que constatez-vous sur les affichages provoqués par les fonctions `Frama_C_show_each*`?
+
+### Partitionnement inter-procédural
+
+Par défaut, le partitionnement est _intra_-procédural, c'est à dire qu'au moment où une fonction où du partitionnement s'est produit retourne, on fusionne les états partitionnés en un seul état abstrait qui est remonté à l'appelant. Si on veut conserver le partitionnement au niveau de l'appelant, il faut utiliser `-eva-interprocedural-history`.
+
+Utiliser cette option. Que constatez-vous sur les messages d'Eva? Lancer l'interface graphique avec ces options et vérifier qu'il y a bien une alarme rouge
+
+### Analyse du code corrigé
+
+Utiliser la version de `set_flag` corrigée telle que proposée sur la page, et vérifier qu'aucune alarme n'est rapportée par Eva.
+
+## CERT C EXP33-C bis
+
+On s'intéresse maintenant à un autre exemple d'utilisation de mémoire non initialisée, cette fois-ci par le biais de la fonction `realloc`. Le code sur lequel on va travailler se trouve dans le fichier [`cert_exp_33_realloc.c`](config/cert_exp_33_realloc.c), et est reproduit ci-dessous:
+
+```c
+#include <stdlib.h>
+#include <stdio.h>
+enum { OLD_SIZE = 10, NEW_SIZE = 20 };
+
+int *resize_array(int *array, size_t count) {
+  if (0 == count) {
+    return 0;
+  }
+
+  int *ret = (int *)realloc(array, count * sizeof(int));
+  if (!ret) {
+    free(array);
+    return 0;
+  }
+
+  return ret;
+}
+
+void func(void) {
+
+  int *array = (int *)malloc(OLD_SIZE * sizeof(int));
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < OLD_SIZE; ++i) {
+    array[i] = i;
+  }
+
+  array = resize_array(array, NEW_SIZE);
+  if (0 == array) {
+    /* Handle error */
+    return;
+  }
+
+  for (size_t i = 0; i < NEW_SIZE; ++i) {
+    printf("%d ", array[i]);
+  }
+}
+```
+
+### Première analyse
+
+Lancer Eva en utilisant le point d'entrée le plus approprié. Quelles sont les alarmes émises? Quelle est celle qui correspond à la lecture
+d'une location mémoire non-initialisée?
+
+### Augmenter la précision des boucles
+
+Comme dans l'exercice précédent, Eva signale une alarme potentielle, mais on ne sait pas s'il s'agit d'une vraie alarme ou d'une fausse. Pour faire apparaître une alarme rouge, il faut améliorer la précision de l'analyse. Ici, ce sont les deux boucles de `func` qui posent problème. Plusieurs possibilités existent pour demander à Eva de garder séparés les états correspondant aux différents tours de boucle. On peut notamment:
+- utiliser l'option `-eva-min-loop-unroll <n>` pour demander à Eva de garder séparés les `n` premiers tours avant de commencer à joindre (et éventuellement élargir) les états;
+- ajouter des annotations `/*@ loop unroll <n>; */` avant les boucles, pour obtenir le même effet, mais pour des boucles particulières;
+- utiliser l'option `-eva-slevel <n>` pour demander à Eva de propager jusqu'à `n` états distincts pour chaque point de programme. Contrairement aux options précédentes, cela s'applique à tous les points de programme, donc les `if` vont aussi provoquer des séparations d'état;
+- utiliser l'option `-eva-precision <n>`, qui positionne un certain nombre d'options améliorant la précision, dont `min-loop-unroll` et `slevel`. `n` peut aller de `0` (le moins précis) à `11` (le plus précis).
+
+Expérimenter au moins une de ces options pour faire apparaitre une alarme rouge pour l'initialisation. Vous pouvez utiliser des appels à
+`Frama_C_show_each_*` dans les boucles pour voir comment la propagation des états est affectée par ces options.
+
+### Analyse précise de `realloc`
+
+L'autre alarme générée par Eva provient du fait qu'avec les options par défaut, Eva ne conserve pas la relation entre la valeur de retour de `realloc` et le statut de son premier argument (plus précisément, `realloc` libère la mémoire du pointeur passé en argument si et seulement si l'allocation réussit, c'est à dire qu'elle retourne un pointeur non-`NULL`). De ce fait, l'analyseur ne peut garantir que le `free(array)` est correct. Si on a utilisé l'option `-eva-slevel` (ou `eva-precision`) à la question précédente, le problème disparait, car les deux états possibles en retour de `realloc` sont gardés séparés. Sinon, il faut forcer Eva à faire cette séparation. Pour cela, on peut utiliser l'annotation `//@ split ret==0;`, juste après l'appel à `realloc`.
+
+Après avoir ajouté cette annotation, vérifier que l'alarme sur `free(array)` disparait bien, même en utilisant `-eva-min-loop-unroll` ou `/*@ loop unroll <n>; */`
+
+### Analyse de la version corrigée
+
+Ajouter la [correction proposée](https://wiki.sei.cmu.edu/confluence/display/c/EXP33-C.+Do+not+read+uninitialized+memory) par le CERT. Pour cela, on ajoute un argument `old_count` à `resize_array`, qui contient la taille initiale de `array`, et si `old_count` est plus petit que `count`, on utilise `memset` (déclarée dans l'en-tête `string.h`) pour initialiser les nouvelles cases à `0`.
+
+Utiliser Eva pour vérifier qu'il n'y a pas d'erreur possible à l'exécution.
+
+## CWE 20
+
+Cet exercice reprend un exemple de vulnerabilité liée à la mauvaise
+validation des entrées utilisateurs, plus spécifiquement la classe
+[CWE20](https://cwe.mitre.org/data/definitions/20.html) de la _Common
+Weakness Enumeration_.  Le code est fourni dans le fichier
+[cwe20.c](config/cwe20.c) et ci-dessous.
+
+```c
+#include <stdio.h>
+#include <stdlib.h>
+void die(const char* s) {
+    printf("%s",s);
+    exit(2);
+}
+
+#define MAX_DIM 15
+
+typedef int board_square_t;
+
+/* board dimensions */
+
+int main () {
+    int m,n, error;
+    board_square_t *board;
+    printf("Please specify the board height: \n");
+    error = scanf("%d", &m);
+    if ( EOF == error ){
+    die("No integer passed: Die evil hacker!\n");
+    }
+    printf("Please specify the board width: \n");
+    error = scanf("%d", &n);
+    if ( EOF == error ){
+    die("No integer passed: Die evil hacker!\n");
+    }
+    if ( m > MAX_DIM || n > MAX_DIM ) {
+    die("Value too large: Die evil hacker!\n");
+    }
+    board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+    for (int i = 0; i < m; i++) {
+        for (int j = 0; j < n; j++) {
+            board[n*i+j] = 0;
+        }
+    }
+    if (board[(m-1)*n] == 0) return 0; else return 1;
+}
+```
+
+### Première analyse
+
+Lancer Frama-C/Eva sur le code. Que peut-on dire des alarmes émises?
+
+### Patch 1
+
+Modifier le code pour éviter le problème décrit dans la page de la CWE20,
+et relancer l'analyse. Modifier éventuellement les options de précision.
+Peut-on supprimer toutes les alarmes restantes?
+
+### Patch 2
+
+Modifier le programme pour qu'on teste si l'allocation a réussi avant d'utiliser
+le bloc mémoire correspondant (si l'allocation échoue, on retourne directement avec
+la valeur `2`), puis relancer l'analyse et regarder si on peut effectivement éviter
+les alarmes.
+
+### Améliorer la précision
+
+Le problème vient du fait que Eva ne garde pas de lien entre la taille du bloc
+alloué par `malloc` et les valeurs de `m` et `n`. Pour pallier à ce problème,
+on peut partitionner l'analyse, _via_ deux directives `//@ split`, de manière à ce que
+pour chaque élément de la partition considère une valeur précise de `m` et de `n`. Il
+conviendra aussi d'utiliser l'option `-eva-alloc-builtin fresh` pour que Eva utilise
+des bases différentes pour chaque élément de la partition.
+
+## libstring
+
+On s'intéresse à la bibliothèque de manipulation de chaines [libstring](https://github.com/cforler/libstring), dont les deux principaux
+fichiers sont [libstring.c](config/libstring.c)
+et [libstring.h](config/libstring.h).
+
+### concat
+
+À l'aide de la fonction `Frama_C_interval` de `__fc_builtin.h` qui prend en entrée deux entiers et renvoie un entier au hasard
+compris entre ces bornes (ce qui sera donc interprété par Eva comme un intervalle), écrire une fonction `main` qui initialise deux
+`string_t` à partir de deux chaines C de 255 caractères aléatoires (entre `1` et `127`) chacune (on n'oubliera pas le `0` terminal
+de chaque chaine C), puis en réalise la concaténation, et imprime le résultat.
+
+Analyser avec Frama-C/Eva ce programme et vérifier l'absence d'erreur à l'exécution.
+
+### replace
+
+Définir de même un contexte aussi générique que possible (mais avec des chaines de taille fixe et relativement réduite) pour étudier avec Eva le comportement de la fonction `string_replace`. Corriger le code si besoin
+
+## Miniz
+
+On s'intéresse dans cet exercice à une bibliothèque de compression, [miniz](https://github.com/richgel999/miniz/),
+et plus précisément à sa dernière release stable, [3.0.2](https://github.com/richgel999/miniz/releases/tag/3.0.2).
+Les fichiers qui vont nous intéresser sont [miniz.h](config/miniz.h), [miniz.c](config/miniz.c) et [example1.c](config/example1.c)
+
+### Compression
+
+#### Première analyse
+
+lancer Eva sur l'exemple: `frama-c -eva miniz.c example1.c`. Que peut-on dire du résultat?
+
+Pour des programmes de taille raisonable, il est généralement nécessaire d'utiliser l'interface
+graphique pour pouvoir naviguer dans le code. En particulier, le greffon Studia permet d'identifier
+les endroits où on a écrit pour la dernière fois dans une location mémoire avant le point
+de programme courant. On l'active par un clic droit sur la location qui nous intéresse, ainsi que
+montré sur l'image ci-dessous:
+
+![studia menu](studia.png)
+
+En partant de la première alarme émise par Eva (qui sont listées dans l'onglet Message de la GUI),
+identifier l'origine de la perte de précision
+
+#### Améliorer la précision
+
+En utilisant judicieusement les options `-eva-slevel <n>` qui permet de garder `n` états
+séparés, `-eva-partition-history <m>`, qui permet de garder séparées les `m` dernières branches
+de l'analyse, et `-eva-split-return-function f:m` qui permet de séparer les états de retour d'une fonction
+`f` en fonction de sa valeur de retour (plus précisément si elle retourne `m` ou autre chose), Réduisez le nombre
+d'alarmes émises par Eva. On pourra bien entendu également utiliser les options vues dans les exercices précédents.
+Arrive-t-on à supprimer toutes les alarmes?
+
+#### Patch
+
+Les dernières alarmes notent un vrai problème dans le code. Toujours à l'aide de Studia, identifiez le(s) point(s)
+où on devrait initialiser les locations en cause, et vérifier qu'on n'a plus d'alarme dans le code ainsi modifié.