diff --git a/Cours/README.md b/Cours/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..f009d855ea7452a08e9e158f9f23f18b3e086f46
--- /dev/null
+++ b/Cours/README.md
@@ -0,0 +1,9 @@
+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.
diff --git a/Cours/config/01-numeric.c b/Cours/config/01-numeric.c
new file mode 100644
index 0000000000000000000000000000000000000000..6c807ed7403240d15e10c15a4d2752c6e2ea3697
--- /dev/null
+++ b/Cours/config/01-numeric.c
@@ -0,0 +1,24 @@
+/* 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;
+ }
+}
diff --git a/Cours/config/02-address.c b/Cours/config/02-address.c
new file mode 100644
index 0000000000000000000000000000000000000000..756a9cb4a518757fd341ebd5722d3b1e6c2b9482
--- /dev/null
+++ b/Cours/config/02-address.c
@@ -0,0 +1,27 @@
+/* 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));
+}
diff --git a/Cours/config/03-address_written.c b/Cours/config/03-address_written.c
new file mode 100644
index 0000000000000000000000000000000000000000..9a2830b874903fd49caba2ece44b6279eca7945e
--- /dev/null
+++ b/Cours/config/03-address_written.c
@@ -0,0 +1,16 @@
+/* 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);
+}
diff --git a/Cours/config/04-cast.c b/Cours/config/04-cast.c
new file mode 100644
index 0000000000000000000000000000000000000000..9a6ac4a5a6f38f95384951b158da2e573aa87efa
--- /dev/null
+++ b/Cours/config/04-cast.c
@@ -0,0 +1,12 @@
+/* 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;
+}
diff --git a/Cours/config/05-domains.c b/Cours/config/05-domains.c
new file mode 100644
index 0000000000000000000000000000000000000000..b901e5f629ea90c85bc480c83fea30e38a14d172
--- /dev/null
+++ b/Cours/config/05-domains.c
@@ -0,0 +1,14 @@
+/* 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;
+}
diff --git a/Cours/config/06-simple.c b/Cours/config/06-simple.c
new file mode 100644
index 0000000000000000000000000000000000000000..b5956944faac6b2e424100c7a2c057fad462dfa1
--- /dev/null
+++ b/Cours/config/06-simple.c
@@ -0,0 +1,13 @@
+/* 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;
+}
diff --git a/Cours/config/07-slevel.c b/Cours/config/07-slevel.c
new file mode 100644
index 0000000000000000000000000000000000000000..3ab8733b405b4369db5cf6e892b1d87052faa07f
--- /dev/null
+++ b/Cours/config/07-slevel.c
@@ -0,0 +1,28 @@
+/* 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--;
+ }
+}
diff --git a/Cours/config/08-split.c b/Cours/config/08-split.c
new file mode 100644
index 0000000000000000000000000000000000000000..591dd3a21f551bc9218699d35caa1ab9c9cf2873
--- /dev/null
+++ b/Cours/config/08-split.c
@@ -0,0 +1,20 @@
+/* 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;
+}
diff --git a/Cours/config/09-context.c b/Cours/config/09-context.c
new file mode 100644
index 0000000000000000000000000000000000000000..a796dbdfc4373666c38dcb513fb68319d32eb4e9
--- /dev/null
+++ b/Cours/config/09-context.c
@@ -0,0 +1,9 @@
+/* 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;
+}
diff --git a/Cours/config/10-context-driver.c b/Cours/config/10-context-driver.c
new file mode 100644
index 0000000000000000000000000000000000000000..3a9419b294617b6f2ff52d1ef8dec17d4ae01e1e
--- /dev/null
+++ b/Cours/config/10-context-driver.c
@@ -0,0 +1,13 @@
+/* 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);
+}
diff --git a/Cours/cours1.pdf b/Cours/cours1.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..6f18b5b7221937e2005f9c9b4fce3d615930d766
Binary files /dev/null and b/Cours/cours1.pdf differ
diff --git a/Cours/cours2.pdf b/Cours/cours2.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..f6de3b8fc7271f996f4e67d8b893d9746ebebdbd
Binary files /dev/null and b/Cours/cours2.pdf differ