Cours et exemples Frama-C

Cours/README.md

+Ce répertoire contient les transparents des cours passés,
+ainsi que les exemples Frama-C/Eva présentés dans le cours 1,
+dans le sous-répertoire config, ce qui permet de les avoir
+automatiquement dans l'image Docker du cours
+(voir  https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl
+pour plus d'information).
+Chaque exemple contient dans un commentaire la ligne
+de commande Frama-C qui permet de faire l'analyse avec
+le niveau de précision voulue.

Cours/config/01-numeric.c

+/* frama-c -eva -main f 01-numeric.c */
+int x, y, t, m;
+double d;
+extern char z;
+char z1;
+
+void f(int c) {
+  if (c) x = 40;
+  for (int i = 0; i <= 40; i++) {
+    Frama_C_show_each_loop(i,y);
+    if (c == i) y = i;
+  }
+  z1 = z;
+  t = z;
+  m = 3;
+  for (int i = 3; i <= 40; i += 4) {
+    if (c == i) m = i;
+  }
+  if (c) {
+    d = 0.25;
+  } else {
+    d = 3.125;
+  }
+}

Cours/config/02-address.c

+/* frama-c -eva -main f 02-address.c */
+#include <stdlib.h>
+extern int* a;
+int *x;
+const char *y;
+int *z;
+int *t;
+int *u;
+
+int p[3];
+const char *string = "foobar";
+
+void f(int c) {
+  if (c) {
+    x = &p[1];
+  } else {
+    x = &p[2];
+  }
+
+  y = string;
+
+  z = (int *)1024;
+
+  t = (int *)((unsigned long)a | 4096);
+
+  u = malloc(sizeof(*u));
+}

Cours/config/03-address_written.c

+/* frama-c -eva 03-address_written.c */
+int X, Y;
+
+int *p;
+
+void f(int c) {
+  int x, y;
+  if (c <= 0) x = 2;
+L:
+  if (c <= 0) y = x + 1;
+  p = c ? &X : &x;
+}
+
+int main(int c) {
+  f(c);
+}

Cours/config/04-cast.c

+/* frama-c -eva -main f 04-cast.c */
+typedef struct {
+  int *monpointeur;
+  short monshort;
+} t;
+void f(int c) {
+  int x = 3;
+  if (c) x = 24;
+  t S = {&x, 12};
+  char *p = (char *)&S;
+  p[2] = 4;
+}

Cours/config/05-domains.c

+/* frama-c -eva 05-domains.c
+   frama-c -eva -eva-domains symbolic-locations,octagon 05-domains.c
+*/
+#include "__fc_builtin.h"
+
+int main () {
+  int x, y;
+  int *p = Frama_C_nondet_ptr(&x,&y);
+  *p = 3;
+  int z = (*p)++;
+  y = Frama_C_interval(0,10);
+  x = y;
+  z = x - y;
+}

Cours/config/06-simple.c

+/* frama-c -eva 06-simple.c */
+int S = 0;
+int T[5];
+int main(void) {
+  int i;
+  int *p = &T[0];
+  /*@ loop unroll 6; */
+  for (i = 0; i < 5; i++) {
+    S = S + i;
+    *p++ = S;
+  }
+  return S;
+}

Cours/config/07-slevel.c

+/* frama-c -eva -eva-slevel 3 07-slevel.c */
+int x, y;
+
+void main(int c) {
+  //@ assert c<=0 || c > 0;
+  if (c) {
+    x = 10;
+  } else {
+    x = 33;
+  }
+  Frama_C_show_each(c);
+  if (!c) {
+    x++;
+  } else {
+    x--;
+  }
+
+  if (c <= 0) {
+    y = 42;
+  } else {
+    y = 36;
+  }
+  if (c > 0) {
+    y++;
+  } else {
+    y--;
+  }
+}

Cours/config/08-split.c

+/* frama-c -eva -eva-slevel 2 -eva-split-return-function f:0 08-split.c */
+extern int c;
+
+int f(int *p) {
+  //@ split c <= 0;
+  if (c <= 0) {
+    *p = 10;
+    return 0;
+  }
+  return -1;
+}
+
+int main() {
+  int x;
+  int res = f(&x);
+  if (!res)
+    x++;
+  else
+    x = 0;
+}

Cours/config/09-context.c

+/* frama-c -eva -eva-context-width 4 -main search 09-context.c */
+int search(char *a, char key) {
+  char *orig = a;
+  while (*a) {
+    if (*a == key) return a - orig;
+    a++;
+  }
+  return -1;
+}

Cours/config/10-context-driver.c

+/* frama-c -eva -eva-precision 3 09-context.c 10-context-driver.c -main driver */
+#include "__fc_builtin.h"
+#include "limits.h"
+
+int search(char *a, char key);
+
+extern char buffer[1024];
+
+int driver() {
+  buffer[1023] = 0;
+  char key = Frama_C_interval(CHAR_MIN, CHAR_MAX);
+  return search(buffer, key);
+}