add test examples for E-ACSL supported and unsupported features

test/c/eacsl/dune → test/c/eacsl/function/dune

@@ -4,4 +4,5 @@
   (package owi)
   max.c
   max_ptr.c
-  integer_dividable.c))
+  integer_dividable.c
+  multi_behaviors.c))

test/c/eacsl/function/multi_behaviors.c

@@ -0,0 +1,44 @@
+#include <limits.h>
+#include <owi.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() {
+    int value = -1;
+    owi_assume(value > INT_MIN);
+    f(value);
+    return 0;
+}

test/c/eacsl/function/multi_behaviors.t

@@ -0,0 +1,2 @@
+  $ owi c --no-value ./multi_behaviors.c --no-value
+  All OK

test/c/eacsl/ghost/case.c

@@ -0,0 +1,19 @@
+#include <owi.h>
+
+int main(void) {
+    int n = owi_i32();
+    //@ ghost int is_case2 = 0;
+    switch (n) {
+        case 0: break;
+        case 1: break;
+        /*@ ghost
+        case 2: {
+            is_case2 = 1;
+            // break; this break is not controlled
+        }
+        */
+        default: break;
+    }
+    //@ assert is_case2 == 0;
+    return 0;
+}

test/c/eacsl/ghost/case.t

@@ -0,0 +1,7 @@
+  $ owi c --e-acsl ./case.c
+  Assert failure: false
+  Model:
+    (model
+      (symbol_0 (i32 2)))
+  Reached problem!
+  [13]

test/c/eacsl/ghost/default.c

@@ -0,0 +1,21 @@
+#include <owi.h>
+
+int main(void) {
+    int n = owi_i32();
+    //@ ghost int is_default = 0;
+    switch (n) {
+        case 0: {
+            break;
+        }
+        case 1: {
+            break;
+        }
+        /*@ ghost default: {
+            is_default = 1;
+            break;
+        }
+        */
+    }
+    //@ assert is_default == 0;
+    return 0;
+}

test/c/eacsl/ghost/default.t

@@ -0,0 +1,7 @@
+  $ owi c --e-acsl ./default.c --no-value
+  Assert failure: false
+  Model:
+    (model
+      (symbol_0 i32))
+  Reached problem!
+  [13]

test/c/eacsl/ghost/dune

@@ -0,0 +1,9 @@
+(cram
+ (deps
+  %{bin:owi}
+  (package owi)
+  case.c
+  default.c
+  else.c
+  global.c
+  parameter.c))

test/c/eacsl/ghost/else.c

@@ -0,0 +1,17 @@
+#include <owi.h>
+
+int main(void) {
+    int x = owi_i32();
+    owi_assume(x >= -1);
+
+    //@ ghost int num;
+
+    if (x >= 0) {
+        //@ ghost num = 42;
+    }
+    //@ ghost else num = 0;  
+
+   //@ assert num == 42;
+
+    return 0;
+}

test/c/eacsl/ghost/else.t

@@ -0,0 +1,7 @@
+  $ owi c --e-acsl ./else.c --no-value
+  Assert failure: false
+  Model:
+    (model
+      (symbol_0 i32))
+  Reached problem!
+  [13]

test/c/eacsl/ghost/global.c

@@ -0,0 +1,21 @@
+#include <owi.h>
+
+//@ ghost int cnt;
+
+/*@ ensures cnt > 10;
+    ensures cnt < 20;
+*/
+void loop(int n) {
+    //@ ghost cnt = 0;
+    while (n--) {
+        //@ ghost cnt += 1;
+    }
+}
+
+int main(void) {
+    int n = owi_i32();
+    owi_assume(n > 10);
+    owi_assume(n <= 20);
+    loop(n);
+    return 0;
+}

test/c/eacsl/ghost/global.t

@@ -0,0 +1,7 @@
+  $ owi c --e-acsl ./global.c
+  Assert failure: false
+  Model:
+    (model
+      (symbol_0 (i32 20)))
+  Reached problem!
+  [13]

test/c/eacsl/ghost/parameter.c

@@ -0,0 +1,55 @@
+#include <owi.h>
+#include <stddef.h>
+#include <stdlib.h>
+
+typedef struct List {
+    int element;
+    struct List* next;
+} List;
+
+void traverse(List* node) /*@ ghost (int length) */ {
+    /*@ loop variant length;
+    */
+    while (node != NULL) {
+        node = node->next;
+        //@ ghost length --;
+    }
+}
+
+List* makeList(int element, List* next) {
+    List *node = (List *)malloc(sizeof(List));
+    if (node == NULL) return NULL;
+    node->element = element;
+    node->next = next;
+    return node;
+}
+
+int size(List* node) {
+    if (node == NULL) return 0;
+    int cnt = 0;
+    while (node != NULL) {
+        node = node->next;
+        cnt ++;
+    }
+    return cnt;
+}
+
+/*@ ghost int ghost_size(List* node) {
+    if (node == NULL) return 0;
+    int cnt = 0;
+    while (node != NULL) {
+        node = node->next;
+        cnt ++;
+    }
+    return cnt;
+}*/
+
+int main(void) {
+    int n = owi_i32();
+    owi_assume(n >= 10);
+    owi_assume(n <= 20);
+    List *node = NULL;
+    while (n--) node = makeList(0, node);
+    traverse(node) /*@ ghost (ghost_size(node)) */ ;
+    return 0;
+}

test/c/eacsl/ghost/parameter.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./parameter.c
+  All OK

test/c/eacsl/loop/array_sum.c

@@ -0,0 +1,18 @@
+#include <owi.h>
+#include <stdlib.h>
+
+int main (void) {
+  int n = 10;
+  int *t;
+  t = (int *)malloc(n * sizeof(int));
+
+  for (int i = 0; i < n; i++) t[i] = owi_i32();
+
+  int sum = 0;
+  /*@ loop invariant 0 <= i <= n;
+    @ loop invariant sum == \sum(0, i - 1, \lambda integer k; t[k]);
+    @ loop variant n - i;
+   */
+  for (int i = 0; i < n; i++) sum += t[i];
+  return 0;
+}

test/c/eacsl/loop/array_sum.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./array_sum.c
+  All OK

test/c/eacsl/loop/dune

@@ -0,0 +1,5 @@
+(cram
+ (deps
+  %{bin:owi}
+  (package owi)
+  array_sum.c))

test/c/eacsl/not-yet-supported/abrupt termination/breaks.c

@@ -0,0 +1,21 @@
+#include <owi.h>
+
+int main(void) {
+    int x = owi_i32();
+    owi_assume(x >= 0);
+    owi_assume(x <= 20);
+    while (x > 0) {
+    /*@ breaks  x % 11 == 0 && x == \old(x);
+      @ ensures (x + 1) % 5 != 0 && (x + 2) % 7 != 0  && (x + 3) % 11 != 0 && x == \old(x) - 3;
+    */
+    {
+        if (x % 11 == 0) break;
+        x--;
+        if (x % 7 == 0) continue;
+        x--;
+        if (x % 5 == 0) return x;
+        x--;
+    }
+    }
+    return 0;
+}

test/c/eacsl/not-yet-supported/abrupt termination/breaks.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./breaks.c
+  All OK

test/c/eacsl/not-yet-supported/abrupt termination/continues.c

@@ -0,0 +1,21 @@
+#include <owi.h>
+
+int main(void) {
+    int x = owi_i32();
+    owi_assume(x >= 0);
+    owi_assume(x <= 20);
+    while (x > 0) {
+    /*@ continues x % 7 == 0  && (x + 1) % 11 != 0 && x == \old(x) - 1;
+      @ ensures   (x + 1) % 5 != 0 && (x + 2) % 7 != 0  && (x + 3) % 11 != 0 && x == \old(x) - 3;
+    */
+    {
+        if (x % 11 == 0) break;
+        x--;
+        if (x % 7 == 0) continue;
+        x--;
+        if (x % 5 == 0) return x;
+        x--;
+    }
+    }
+    return 0;
+}

test/c/eacsl/not-yet-supported/abrupt termination/continues.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./continues.c
+  All OK

test/c/eacsl/not-yet-supported/abrupt termination/dune

@@ -0,0 +1,8 @@
+(cram
+ (deps
+  %{bin:owi}
+  (package owi)
+  breaks.c
+  continues.c
+  exits.c
+  returns.c))

test/c/eacsl/not-yet-supported/abrupt termination/exits.c

@@ -0,0 +1,20 @@
+#include <owi.h>
+#include <stdlib.h>
+
+int status = 0;
+
+/*@ exits  !cond && status == val && \exit_status == 0;
+    ensures cond && status == \old(status);
+*/
+void may_exit(int cond, int val) {
+    if (!cond) {
+        status = val;
+        exit(0);
+    }
+}
+
+int main(void) {
+    int cond = owi_i32(), val = owi_i32();
+    may_exit(cond, val);
+    return 0;
+}

test/c/eacsl/not-yet-supported/abrupt termination/exits.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./exits.c
+  All OK

test/c/eacsl/not-yet-supported/abrupt termination/returns.c

@@ -0,0 +1,21 @@
+#include <owi.h>
+
+int main(void) {
+    int x = owi_i32();
+    owi_assume(x >= 0);
+    owi_assume(x <= 20);
+    while (x > 0) {
+    /*@ returns \result % 5 == 0 && (\result + 1) % 7 != 0 && (\result + 2) % 11 != 0 && \result == \at(x, Pre) - 2;
+      @ ensures (x + 1) % 5 != 0 && (x + 2) % 7 != 0  && (x + 3) % 11 != 0 && x == \old(x) - 3;
+    */
+    {
+        if (x % 11 == 0) break;
+        x--;
+        if (x % 7 == 0) continue;
+        x--;
+        if (x % 5 == 0) return x;
+        x--;
+    }
+    }
+    return 0;
+}

test/c/eacsl/not-yet-supported/abrupt termination/returns.t

@@ -0,0 +1,2 @@
+  $ owi c --e-acsl ./returns.c
+  All OK

test/c/eacsl/not-yet-supported/data invariant/dune

@@ -0,0 +1,8 @@
+(cram
+ (deps
+  %{bin:owi}
+  (package owi)
+  global.c
+  type.c
+  strong_global.c
+  strong_type.c))

test/c/eacsl/not-yet-supported/data invariant/global.c

@@ -0,0 +1,16 @@
+#include <owi.h>
+
+int col;
+//@ global invariant I : 0 <= col <= 100;
+
+void increment(void) {
+    col += 1;
+}
+
+int main(void) {
+    col = owi_i32();
+    owi_assume(0 <= col);
+    owi_assume(col <= 100);
+    increment();
+    return 0;
+}