diff --git a/CR-TP5/.gitkeep b/CR-TP5/.gitkeep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/TP5/Exo1/first-example.c b/TP5/Exo1/first-example.c
new file mode 100644
index 0000000000000000000000000000000000000000..458d1ed01c3af8c7af485457ea5b9a61c6f2a1d5
--- /dev/null
+++ b/TP5/Exo1/first-example.c
@@ -0,0 +1,41 @@
+#include <limits.h>
+#include "__fc_builtin.h"
+
+/*@
+ ensures \result >= 0;
+*/
+int abs(int val)
+{
+ if (val < 0)
+ return -val;
+ return val;
+}
+
+/*@ ensures \result == a + b;
+ */
+int add(int a, int b)
+{
+ return a + b;
+}
+
+/*@ ensures \result == a/b;
+ */
+int div(int a, int b)
+{
+ return a / b;
+}
+
+int main(void)
+{
+ int a = abs(42);
+ int b = abs(-42);
+ int c = abs(-74);
+ int d = add(a, c);
+ int e = add(d, d);
+ // b = add(INT_MAX,42); //cas d’erreur 1
+ // a = abs(INT_MIN); //cas d’erreur 2
+ a = div(4, 8);
+ b = div(17, -12);
+ // c = div(15,0); //cas d’erreur 3
+ a = div(-12, 54);
+}
\ No newline at end of file
diff --git a/TP5/Exo2/max.c b/TP5/Exo2/max.c
new file mode 100644
index 0000000000000000000000000000000000000000..a1888642c0bfcdb3c3b52838f3b02295eda5a4eb
--- /dev/null
+++ b/TP5/Exo2/max.c
@@ -0,0 +1,9 @@
+#include "max.h"
+
+int max(int a, int b)
+{
+ int res = a;
+ if (res < b)
+ res = b;
+ return res;
+}
\ No newline at end of file
diff --git a/TP5/Exo2/max.h b/TP5/Exo2/max.h
new file mode 100644
index 0000000000000000000000000000000000000000..e93187390606a53f2c50b44143146b405817aa7a
--- /dev/null
+++ b/TP5/Exo2/max.h
@@ -0,0 +1,4 @@
+
+/*Put your specification here.
+*/
+int max(int a, int b);
\ No newline at end of file
diff --git a/TP5/Exo2/max_5.c b/TP5/Exo2/max_5.c
new file mode 100644
index 0000000000000000000000000000000000000000..5eb292f81c4351186e719f07f3c0124e06fcbc11
--- /dev/null
+++ b/TP5/Exo2/max_5.c
@@ -0,0 +1,15 @@
+#include "max_5.h"
+
+int max(int a, int b, int c, int d, int e)
+{
+ int res = a;
+ if (res < b)
+ res = b;
+ if (res < c)
+ res = c;
+ if (res < d)
+ res = d;
+ if (res < e)
+ res = e;
+ return res;
+}
\ No newline at end of file
diff --git a/TP5/Exo2/max_5.h b/TP5/Exo2/max_5.h
new file mode 100644
index 0000000000000000000000000000000000000000..dca93e78f5f84f95ea406bd3ee0ac6540bd06fb0
--- /dev/null
+++ b/TP5/Exo2/max_5.h
@@ -0,0 +1,4 @@
+
+/*Put your specification here.
+ */
+int max(int a, int b, int c, int d, int e);
\ No newline at end of file
diff --git a/TP5/Exo2/max_wrong1.c b/TP5/Exo2/max_wrong1.c
new file mode 100644
index 0000000000000000000000000000000000000000..5aa5408fa6d82683560dc8c864d27f128c9ebb9d
--- /dev/null
+++ b/TP5/Exo2/max_wrong1.c
@@ -0,0 +1,6 @@
+#include "max.h"
+
+int max(int a, int b)
+{
+ return a;
+}
\ No newline at end of file
diff --git a/TP5/Exo2/max_wrong2.c b/TP5/Exo2/max_wrong2.c
new file mode 100644
index 0000000000000000000000000000000000000000..85ed233d5962131867ba045a6c667db2b1439d90
--- /dev/null
+++ b/TP5/Exo2/max_wrong2.c
@@ -0,0 +1,7 @@
+#include "max.h"
+#include "limits.h"
+
+int max(int a, int b)
+{
+ return INT_MAX;
+}
\ No newline at end of file
diff --git a/TP5/Exo2/silly-max.c b/TP5/Exo2/silly-max.c
new file mode 100644
index 0000000000000000000000000000000000000000..a42a4895f6dcd7167a677e430d11a92464d7f95b
--- /dev/null
+++ b/TP5/Exo2/silly-max.c
@@ -0,0 +1,25 @@
+#include "max.h"
+
+int max(int a, int b)
+{
+ if (a == 0 && b == 0)
+ return 0;
+ if (a <= 0 && b >= 0)
+ return b;
+ if (a > 42 && b <= 25)
+ return a;
+ if (a >= 0 && b <= 0)
+ return a;
+ if (a - b > 4)
+ return a;
+ if (a - b < 1)
+ return b;
+ if (a == b + 1)
+ return a;
+ if (a <= b + 4)
+ if (a + 1 < b)
+ return b;
+ else
+ return a;
+ return 42;
+}
\ No newline at end of file
diff --git a/TP5/Exo3/calling-functions.c b/TP5/Exo3/calling-functions.c
new file mode 100644
index 0000000000000000000000000000000000000000..df97db92f93091bc06451d195242bdcb1c7341eb
--- /dev/null
+++ b/TP5/Exo3/calling-functions.c
@@ -0,0 +1,47 @@
+#include "plus_one.h"
+#include "div.h"
+
+int good_call_1(void)
+{
+ return plus_one(4);
+}
+
+int bad_call_1(void)
+{
+ return plus_one(-345);
+}
+
+int bad_call_2(void)
+{
+ return plus_one(INT_MAX);
+}
+
+int good_call_2(void)
+{
+ return div(45, 73);
+}
+
+int good_call_3(void)
+{
+ return div(0, 74);
+}
+
+int bad_call_3(void)
+{
+ return div(74, 0);
+}
+
+int good_call_4(void)
+{
+ return div(INT_MAX, INT_MIN);
+}
+
+int good_call_5(void)
+{
+ return div(INT_MAX, -1);
+}
+
+int bad_call_4(void)
+{
+ return div(INT_MIN, -1);
+}
\ No newline at end of file
diff --git a/TP5/Exo3/div.c b/TP5/Exo3/div.c
new file mode 100644
index 0000000000000000000000000000000000000000..531833bfd3490bf59e6d59b9865562d1bfa91ee6
--- /dev/null
+++ b/TP5/Exo3/div.c
@@ -0,0 +1,6 @@
+#include "div.h"
+
+int div(int a, int b)
+{
+ return a / b;
+}
\ No newline at end of file
diff --git a/TP5/Exo3/div.h b/TP5/Exo3/div.h
new file mode 100644
index 0000000000000000000000000000000000000000..1a1bbb680c9a9aad6feb96aae933a96b9adf99f9
--- /dev/null
+++ b/TP5/Exo3/div.h
@@ -0,0 +1,5 @@
+#include "limits.h"
+
+/*@ ensures \result == a/b;
+*/
+int div(int a, int b);
\ No newline at end of file
diff --git a/TP5/Exo3/plus_one.c b/TP5/Exo3/plus_one.c
new file mode 100644
index 0000000000000000000000000000000000000000..79d9baeff6d6a2f1320485656f16013b29f76908
--- /dev/null
+++ b/TP5/Exo3/plus_one.c
@@ -0,0 +1,6 @@
+#include "plus_one.h"
+
+int plus_one(int a)
+{
+ return a + 1;
+}
\ No newline at end of file
diff --git a/TP5/Exo3/plus_one.h b/TP5/Exo3/plus_one.h
new file mode 100644
index 0000000000000000000000000000000000000000..9ee47187c0519309e7c052322c5f73c8620f47b8
--- /dev/null
+++ b/TP5/Exo3/plus_one.h
@@ -0,0 +1,4 @@
+
+/*@ ensures \result >= 0;
+*/
+int plus_one(int a);
\ No newline at end of file
diff --git a/TP5/Exo4/affine.c b/TP5/Exo4/affine.c
new file mode 100644
index 0000000000000000000000000000000000000000..f2a09f5a73fd5bbd640d5e3ac55be5e798102941
--- /dev/null
+++ b/TP5/Exo4/affine.c
@@ -0,0 +1,6 @@
+#include "affine.h"
+
+int f(int a, int b, int x)
+{
+ return a * x + b;
+}
\ No newline at end of file
diff --git a/TP5/Exo4/affine.h b/TP5/Exo4/affine.h
new file mode 100644
index 0000000000000000000000000000000000000000..3b4bfa334a600a5391525c13aede53113115ac2a
--- /dev/null
+++ b/TP5/Exo4/affine.h
@@ -0,0 +1,4 @@
+#include "limits.h"
+
+/* Écrivez ici votre spécification. Attention, elle doit permettre de prouver les assertions RTE.*/
+int f(int a,int b,int x);
\ No newline at end of file
diff --git a/TP5/Exo5/behavior-example.c b/TP5/Exo5/behavior-example.c
new file mode 100644
index 0000000000000000000000000000000000000000..1f1fec51484f50f0c95cd818f571c15c9208ad81
--- /dev/null
+++ b/TP5/Exo5/behavior-example.c
@@ -0,0 +1,27 @@
+#include "limits.h"
+
+/*@ requires a < INT_MAX;
+ behavior div:
+ assumes a <= 0;
+ requires b != 0;
+ ensures \result == a/b;
+
+ behavior add:
+ assumes a > 0 && b <= 0;
+ ensures \result == a+b;
+
+ behavior sub:
+ assumes a > 0 && b >= 0;
+ ensures \result == a-b;
+
+ complete behaviors;
+ disjoint behaviors div,add;
+*/
+int addOrDiv(int a, int b)
+{
+ if (a <= 0)
+ return a / b;
+ if (b <= 0)
+ return a + b;
+ return a - b;
+}
\ No newline at end of file
diff --git a/TP5/Exo5/predicate-example.c b/TP5/Exo5/predicate-example.c
new file mode 100644
index 0000000000000000000000000000000000000000..3f5be2138a3993cfe4653f1530a9010ac81ffaa0
--- /dev/null
+++ b/TP5/Exo5/predicate-example.c
@@ -0,0 +1,16 @@
+
+/*@ predicate inInterval(integer a, integer b, integer c) = a >= b && a <= c;
+
+ predicate fourInOrder(integer a, integer b, integer c, integer d) = inInterval(b,a,c) && inInterval(c,b,d);
+
+ predicate controlledEquality(integer a, integer b, boolean c) = a == b || c;
+*/
+
+/*@ requires inInterval(a,b,c);
+ requires inInterval(c,a,d);
+ ensures fourInOrder(\result,a,c,d);
+*/
+int toto(int a, int b, int c, int d)
+{
+ return b;
+}
\ No newline at end of file
diff --git a/TP5/Exo5/result-case.c b/TP5/Exo5/result-case.c
new file mode 100644
index 0000000000000000000000000000000000000000..b5d30a3f517a30ff33135aa6f22c4bed6641c6e5
--- /dev/null
+++ b/TP5/Exo5/result-case.c
@@ -0,0 +1,15 @@
+#include "result-case.h"
+
+int caseResult(int a, int b, int c)
+{
+ if (a == b || b == c || a == c)
+ return 0;
+ if (a <= b && a <= c)
+ return 1;
+ if (b <= a && a <= c)
+ return 2;
+ if (c <= a && c <= b)
+ return 3;
+ // Dans quel ordre sont rangés a,b et c ici ?
+ return 2;
+}
\ No newline at end of file
diff --git a/TP5/Exo5/result-case.h b/TP5/Exo5/result-case.h
new file mode 100644
index 0000000000000000000000000000000000000000..208c8aa131a1983c62f58acbd0091aef4e542be7
--- /dev/null
+++ b/TP5/Exo5/result-case.h
@@ -0,0 +1,6 @@
+
+/* Put your specification here.
+
+Attention, la spécification à trouver ici n’est pas une paraphrase du code. Demandez-vous, pour chaque résultat quel est la description la plus courte dans laquelle ce résultat est renvoyé.
+*/
+int caseResult(int a, int b, int c);
\ No newline at end of file
diff --git a/TP5/Exo6/exo6.h b/TP5/Exo6/exo6.h
new file mode 100644
index 0000000000000000000000000000000000000000..b8a9b48ba01a034485584891b9169a1c39df6878
--- /dev/null
+++ b/TP5/Exo6/exo6.h
@@ -0,0 +1,30 @@
+#include "limits.h"
+
+/**
+ * @brief Computes the min of these arguments.
+ *
+ * @param a an integer
+ * @param b an integer
+ * @param c an integer
+ * @return int The smallest value among a, b and c.
+ */
+int min(int a, int b, int c);
+
+/**
+ * @brief Computes the next step of @p a in the Syracuse sequence, i.e., its quotient by 2 if @p a is even, and 3 * @p a +1 otherwise.
+ *
+ * @param a an integer.
+ * @return int The next value in the Syracuse sequence.
+ */
+int syracuseStep(int a);
+
+/**
+ * @brief Computes the rounding of the (real) quotient of a by b, i.e. the closest integer to the quotient. We will accept a function that does that only for positive integers (remember the C int division is not the Euclidean division). As a bonus, you might implement a function that works for any pair of integer (such that the quotient is defined of course).
+ *
+ * @param a the dividend
+ * @param b the diviser
+ * @return int The rounding of a/.b.
+ * @pre a and b are positive (or not, depending of your implementation).
+ * @pre b is not 0.
+ */
+int roundedDiv(int a, int b);
\ No newline at end of file