[eacsl:examples] Add examples for function and statement contracts

src/plugins/e-acsl/examples/contracts/function_contract.c

+#include <limits.h>
+
+/*@
+    requires value > INT_MIN;
+    ensures \result == value;
+
+    behavior neg:
+        assumes value < 0;
+        requires value < 1;
+        ensures \result == value;
+
+    behavior pos:
+        assumes value >= 0;
+        requires value > -1;
+        ensures \result == value;
+
+    behavior odd:
+        assumes value % 2 == 1;
+        requires (value % 2) - 1 == 0;
+        ensures \result == value;
+
+    behavior even:
+        assumes value % 2 == 0;
+        requires (value % 2) + 1 == 1;
+        ensures \result == value;
+
+    complete behaviors neg, pos;
+    complete behaviors odd, even;
+    complete behaviors;
+
+    disjoint behaviors neg, pos;
+    disjoint behaviors odd, even;
+*/
+int f(int value) {
+    return value;
+}
+
+int main() {
+    f(3);
+    return 0;
+}
+

src/plugins/e-acsl/examples/contracts/statement_contract.c

+#include <limits.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <time.h>
+
+int main() {
+    int value, sign, result;
+
+    srand(time(NULL));
+    value = rand();
+    sign = rand();
+    if (sign % 2) {
+        value = -value;
+    }
+
+    /*@
+        requires value > INT_MIN;
+        assigns result;
+        ensures result >= 0;
+
+        behavior pos:
+            assumes value >= 0;
+            ensures result == value;
+
+        behavior neg:
+            assumes value < 0;
+            ensures result == -value;
+
+        complete behaviors;
+        disjoint behaviors;
+    */
+    if (value < 0) {
+        result = -value;
+    } else {
+        result = value;
+    }
+
+    printf("Value: %d, Result: %d\n", value, result);
+
+    return 0;
+}
+