From 170f4a29bf874b3cca76b64ef61ecaa0dfba8670 Mon Sep 17 00:00:00 2001
From: Arnaud LABOUREL <arnaud.labourel@lis-lab.fr>
Date: Fri, 7 Feb 2025 14:38:51 +0100
Subject: [PATCH] Added c files for TP frama-c
---
CR-TP5/.gitkeep | 0
TP5/Exo1/first-example.c | 41 +++++++++++++++++++++++++++++++
TP5/Exo2/max.c | 9 +++++++
TP5/Exo2/max.h | 4 +++
TP5/Exo2/max_5.c | 15 ++++++++++++
TP5/Exo2/max_5.h | 4 +++
TP5/Exo2/max_wrong1.c | 6 +++++
TP5/Exo2/max_wrong2.c | 7 ++++++
TP5/Exo2/silly-max.c | 25 +++++++++++++++++++
TP5/Exo3/calling-functions.c | 47 ++++++++++++++++++++++++++++++++++++
TP5/Exo3/div.c | 6 +++++
TP5/Exo3/div.h | 5 ++++
TP5/Exo3/plus_one.c | 6 +++++
TP5/Exo3/plus_one.h | 4 +++
TP5/Exo4/affine.c | 6 +++++
TP5/Exo4/affine.h | 4 +++
TP5/Exo5/behavior-example.c | 27 +++++++++++++++++++++
TP5/Exo5/predicate-example.c | 16 ++++++++++++
TP5/Exo5/result-case.c | 15 ++++++++++++
TP5/Exo5/result-case.h | 6 +++++
TP5/Exo6/exo6.h | 30 +++++++++++++++++++++++
21 files changed, 283 insertions(+)
create mode 100644 CR-TP5/.gitkeep
create mode 100644 TP5/Exo1/first-example.c
create mode 100644 TP5/Exo2/max.c
create mode 100644 TP5/Exo2/max.h
create mode 100644 TP5/Exo2/max_5.c
create mode 100644 TP5/Exo2/max_5.h
create mode 100644 TP5/Exo2/max_wrong1.c
create mode 100644 TP5/Exo2/max_wrong2.c
create mode 100644 TP5/Exo2/silly-max.c
create mode 100644 TP5/Exo3/calling-functions.c
create mode 100644 TP5/Exo3/div.c
create mode 100644 TP5/Exo3/div.h
create mode 100644 TP5/Exo3/plus_one.c
create mode 100644 TP5/Exo3/plus_one.h
create mode 100644 TP5/Exo4/affine.c
create mode 100644 TP5/Exo4/affine.h
create mode 100644 TP5/Exo5/behavior-example.c
create mode 100644 TP5/Exo5/predicate-example.c
create mode 100644 TP5/Exo5/result-case.c
create mode 100644 TP5/Exo5/result-case.h
create mode 100644 TP5/Exo6/exo6.h
diff --git a/CR-TP5/.gitkeep b/CR-TP5/.gitkeep
new file mode 100644
index 0000000..e69de29
diff --git a/TP5/Exo1/first-example.c b/TP5/Exo1/first-example.c
new file mode 100644
index 0000000..458d1ed
--- /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 0000000..a188864
--- /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 0000000..e931873
--- /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 0000000..5eb292f
--- /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 0000000..dca93e7
--- /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 0000000..5aa5408
--- /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 0000000..85ed233
--- /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 0000000..a42a489
--- /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 0000000..df97db9
--- /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 0000000..531833b
--- /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 0000000..1a1bbb6
--- /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 0000000..79d9bae
--- /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 0000000..9ee4718
--- /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 0000000..f2a09f5
--- /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 0000000..3b4bfa3
--- /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 0000000..1f1fec5
--- /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 0000000..3f5be21
--- /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 0000000..b5d30a3
--- /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 0000000..208c8aa
--- /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 0000000..b8a9b48
--- /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
--
GitLab