TP5/Exo1/first-example.c

+#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

TP5/Exo2/max.c

+#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

TP5/Exo2/max.h

+
+/*Put your specification here.
+*/
+int max(int a, int b);
\ No newline at end of file

TP5/Exo2/max_5.c

+#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

TP5/Exo2/max_5.h

+
+/*Put your specification here.
+ */
+int max(int a, int b, int c, int d, int e);
\ No newline at end of file

TP5/Exo2/max_wrong1.c

+#include "max.h"
+
+int max(int a, int b)
+{
+	return a;
+}
\ No newline at end of file

TP5/Exo2/max_wrong2.c

+#include "max.h"
+#include "limits.h"
+
+int max(int a, int b)
+{
+	return INT_MAX;
+}
\ No newline at end of file

TP5/Exo2/silly-max.c

+#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

TP5/Exo3/calling-functions.c

+#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

TP5/Exo3/div.c

+#include "div.h"
+
+int div(int a, int b)
+{
+    return a / b;
+}
\ No newline at end of file

TP5/Exo3/div.h

+#include "limits.h"
+
+/*@ ensures \result == a/b;
+*/
+int div(int a, int b);
\ No newline at end of file

TP5/Exo3/plus_one.c

+#include "plus_one.h"
+
+int plus_one(int a)
+{
+	return a + 1;
+}
\ No newline at end of file

TP5/Exo3/plus_one.h

+
+/*@ ensures \result >= 0;
+*/
+int plus_one(int a);
\ No newline at end of file

TP5/Exo4/affine.c

+#include "affine.h"
+
+int f(int a, int b, int x)
+{
+  return a * x + b;
+}
\ No newline at end of file

TP5/Exo4/affine.h

+#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

TP5/Exo5/behavior-example.c

+#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

TP5/Exo5/predicate-example.c

+
+/*@ 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

TP5/Exo5/result-case.c

+#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

TP5/Exo5/result-case.h

+
+/* 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