[eacsl] Update tests

src/plugins/e-acsl/tests/constructs/decrease.i

+/* run.config_ci, run.config_dev
+   STDOPT: +"-eva-ignore-recursive-calls -eva-slevel 7"
+ */
+
+// Test that the last iteration of the variant can be negative
+int f(int x) {
+  /*@ loop variant x; */
+  while (x >= 0) {
+    x -= 2;
+  }
+  return x;
+}
+
+// Test variant with general measure
+/*@ predicate lexico(integer x, integer y) =
+      x > y && 0 <= x; */
+int g(int x) {
+  /*@ loop variant x for lexico; */
+  while (x >= 0) {
+    x -= 2;
+  }
+  return x;
+}
+
+// Test classic variant
+/*@ requires n <= 12; */
+int fact(int n) {
+  int result = n;
+  /*@ loop invariant n >= 1;
+      loop variant n; */
+  while (n > 1) {
+    result *= (n - 1);
+    --n;
+  }
+  return result;
+}
+
+// Test decreases on recursive function
+/*@ decreases n; */
+int fib(int n) {
+  if (n == 1) return 1;
+  if (n <= 0) return 0;
+  return fib(n - 1) + fib(n - 2);
+}
+
+// Test decreases on mutually recursive functions
+int odd(int);
+/*@ requires n >= 0;
+    decreases n; */
+int even(int n) {
+  if (n == 0) return 1;
+  return odd(n - 1);
+}
+/*@ requires n >= 0;
+    decreases n; */
+int odd(int n) {
+  if (n == 0) return 0;
+  return even(n - 1);
+}
+
+int main() {
+  int f10 = f(10);
+  //@ assert f10 == -2;
+  int f7 = f(7);
+  //@ assert f7 == -1;
+  int g10 = g(10);
+  //@ assert g10 == -2;
+  int g7 = g(7);
+  //@ assert g7 == -1;
+
+  int fact7 = fact(7);
+  //@ assert fact7 == 5040;
+
+  int fib7 = fib(7);
+  //@ assert fib7 == 13;
+
+  int even7 = even(7);
+  //@ assert even7 == 0;
+  int even10 = even(10);
+  //@ assert even10 == 1;
+  int odd7 = odd(7);
+  //@ assert odd7 == 1;
+  int odd10 = odd(10);
+  //@ assert odd10 == 0;
+
+  return 0;
+}

src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] tests/constructs/decrease.i:50: Warning: 
+  E-ACSL construct `decreases clause' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/constructs/decrease.i:47: Warning: 
+  E-ACSL construct `decreases clause' is not yet supported.
+  Ignoring annotation.
+[e-acsl] tests/constructs/decrease.i:40: Warning: 
+  E-ACSL construct `decreases clause' is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva] tests/constructs/decrease.i:43: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
+                                           __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
+                                           main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva] tests/constructs/decrease.i:43: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_fib (__gen_e_acsl_fib <- fib :: tests/constructs/decrease.i:40 <-
+                                           __gen_e_acsl_fib :: tests/constructs/decrease.i:74 <-
+                                           main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:43: Warning: 
+  signed overflow.
+  assert -2147483648 ≤ tmp + tmp_0;
+  (tmp from fib(n - 1), tmp_0 from fib(n - 2))
+[eva:alarm] tests/constructs/decrease.i:43: Warning: 
+  signed overflow.
+  assert tmp + tmp_0 ≤ 2147483647;
+  (tmp from fib(n - 1), tmp_0 from fib(n - 2))
+[eva:alarm] tests/constructs/decrease.i:75: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:58: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
+                                             __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
+                                             even :: tests/constructs/decrease.i:50 <-
+                                             __gen_e_acsl_even :: tests/constructs/decrease.i:77 <-
+                                             main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:78: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:58: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_even (__gen_e_acsl_even <- odd :: tests/constructs/decrease.i:47 <-
+                                             __gen_e_acsl_odd :: tests/constructs/decrease.i:52 <-
+                                             even :: tests/constructs/decrease.i:50 <-
+                                             __gen_e_acsl_even :: tests/constructs/decrease.i:79 <-
+                                             main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:80: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:52: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
+                                           __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
+                                           odd :: tests/constructs/decrease.i:47 <-
+                                           __gen_e_acsl_odd :: tests/constructs/decrease.i:81 <-
+                                           main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:82: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva] tests/constructs/decrease.i:52: Warning: 
+  recursive call during value analysis
+  of __gen_e_acsl_odd (__gen_e_acsl_odd <- even :: tests/constructs/decrease.i:50 <-
+                                           __gen_e_acsl_even :: tests/constructs/decrease.i:58 <-
+                                           odd :: tests/constructs/decrease.i:47 <-
+                                           __gen_e_acsl_odd :: tests/constructs/decrease.i:83 <-
+                                           main).
+  Assuming the call has no effect. The analysis will be unsound.
+[eva:alarm] tests/constructs/decrease.i:84: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.

src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern int __e_acsl_sound_verdict;
+
+int f(int x)
+{
+  int __gen_e_acsl_old_variant;
+  /*@ loop variant x; */
+  while (1) {
+    __gen_e_acsl_old_variant = x;
+    if (! (x >= 0)) break;
+    x -= 2;
+    __e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","f",
+                    "(old x) \342\211\245 0","tests/constructs/decrease.i",8);
+    __e_acsl_assert(__gen_e_acsl_old_variant > x,1,"Variant","f",
+                    "(old x) > x","tests/constructs/decrease.i",8);
+  }
+  return x;
+}
+
+/*@ predicate lexico(ℤ x, ℤ y) = x > y ∧ 0 ≤ x;
+
+*/
+int __gen_e_acsl_lexico(int x, int y);
+
+int g(int x)
+{
+  int __gen_e_acsl_old_variant;
+  /*@ loop variant x for lexico; */
+  while (1) {
+    __gen_e_acsl_old_variant = x;
+    if (! (x >= 0)) break;
+    x -= 2;
+    {
+      int __gen_e_acsl_lexico_2;
+      __gen_e_acsl_lexico_2 = __gen_e_acsl_lexico(__gen_e_acsl_old_variant,x);
+      __e_acsl_assert(__gen_e_acsl_lexico_2,1,"Variant","g",
+                      "lexico(old x, x)","tests/constructs/decrease.i",19);
+    }
+  }
+  return x;
+}
+
+/*@ requires n ≤ 12; */
+int __gen_e_acsl_fact(int n);
+
+int fact(int n)
+{
+  int __gen_e_acsl_old_variant;
+  int result = n;
+  __e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
+                  "tests/constructs/decrease.i",29);
+  /*@ loop invariant n ≥ 1;
+      loop variant n; */
+  while (1) {
+    __gen_e_acsl_old_variant = n;
+    if (! (n > 1)) break;
+    result *= n - 1;
+    n --;
+    __e_acsl_assert(n >= 1,1,"Invariant","fact","n >= 1",
+                    "tests/constructs/decrease.i",29);
+    __e_acsl_assert(__gen_e_acsl_old_variant >= 0,1,"Variant","fact",
+                    "(old n) \342\211\245 0","tests/constructs/decrease.i",
+                    31);
+    __e_acsl_assert(__gen_e_acsl_old_variant > n,1,"Variant","fact",
+                    "(old n) > n","tests/constructs/decrease.i",31);
+  }
+  return result;
+}
+
+/*@ decreases n; */
+int __gen_e_acsl_fib(int n);
+
+int fib(int n)
+{
+  int __retres;
+  int tmp;
+  int tmp_0;
+  if (n == 1) {
+    __retres = 1;
+    goto return_label;
+  }
+  if (n <= 0) {
+    __retres = 0;
+    goto return_label;
+  }
+  tmp = __gen_e_acsl_fib(n - 1);
+  tmp_0 = __gen_e_acsl_fib(n - 2);
+  /*@ assert Eva: signed_overflow: -2147483648 ≤ tmp + tmp_0; */
+  /*@ assert Eva: signed_overflow: tmp + tmp_0 ≤ 2147483647; */
+  __retres = tmp + tmp_0;
+  return_label: return __retres;
+}
+
+/*@ requires n ≥ 0;
+    decreases n; */
+int __gen_e_acsl_odd(int n);
+
+int odd(int n);
+
+/*@ requires n ≥ 0;
+    decreases n; */
+int __gen_e_acsl_even(int n);
+
+int even(int n)
+{
+  int __retres;
+  int tmp;
+  if (n == 0) {
+    __retres = 1;
+    goto return_label;
+  }
+  tmp = __gen_e_acsl_odd(n - 1);
+  __retres = tmp;
+  return_label: return __retres;
+}
+
+int odd(int n)
+{
+  int __retres;
+  int tmp;
+  if (n == 0) {
+    __retres = 0;
+    goto return_label;
+  }
+  tmp = __gen_e_acsl_even(n - 1);
+  __retres = tmp;
+  return_label: return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  int f10 = f(10);
+  __e_acsl_assert(f10 == -2,1,"Assertion","main","f10 == -2",
+                  "tests/constructs/decrease.i",63);
+  /*@ assert f10 ≡ -2; */ ;
+  int f7 = f(7);
+  __e_acsl_assert(f7 == -1,1,"Assertion","main","f7 == -1",
+                  "tests/constructs/decrease.i",65);
+  /*@ assert f7 ≡ -1; */ ;
+  int g10 = g(10);
+  __e_acsl_assert(g10 == -2,1,"Assertion","main","g10 == -2",
+                  "tests/constructs/decrease.i",67);
+  /*@ assert g10 ≡ -2; */ ;
+  int g7 = g(7);
+  __e_acsl_assert(g7 == -1,1,"Assertion","main","g7 == -1",
+                  "tests/constructs/decrease.i",69);
+  /*@ assert g7 ≡ -1; */ ;
+  int fact7 = __gen_e_acsl_fact(7);
+  __e_acsl_assert(fact7 == 5040,1,"Assertion","main","fact7 == 5040",
+                  "tests/constructs/decrease.i",72);
+  /*@ assert fact7 ≡ 5040; */ ;
+  int fib7 = __gen_e_acsl_fib(7);
+  __e_acsl_assert(fib7 == 13,1,"Assertion","main","fib7 == 13",
+                  "tests/constructs/decrease.i",75);
+  /*@ assert fib7 ≡ 13; */ ;
+  int even7 = __gen_e_acsl_even(7);
+  __e_acsl_assert(even7 == 0,1,"Assertion","main","even7 == 0",
+                  "tests/constructs/decrease.i",78);
+  /*@ assert even7 ≡ 0; */ ;
+  int even10 = __gen_e_acsl_even(10);
+  __e_acsl_assert(even10 == 1,1,"Assertion","main","even10 == 1",
+                  "tests/constructs/decrease.i",80);
+  /*@ assert even10 ≡ 1; */ ;
+  int odd7 = __gen_e_acsl_odd(7);
+  __e_acsl_assert(odd7 == 1,1,"Assertion","main","odd7 == 1",
+                  "tests/constructs/decrease.i",82);
+  /*@ assert odd7 ≡ 1; */ ;
+  int odd10 = __gen_e_acsl_odd(10);
+  __e_acsl_assert(odd10 == 0,1,"Assertion","main","odd10 == 0",
+                  "tests/constructs/decrease.i",84);
+  /*@ assert odd10 ≡ 0; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ requires n ≥ 0;
+    decreases n; */
+int __gen_e_acsl_even(int n)
+{
+  int __retres;
+  __e_acsl_assert(n >= 0,1,"Precondition","even","n >= 0",
+                  "tests/constructs/decrease.i",48);
+  __retres = even(n);
+  return __retres;
+}
+
+/*@ requires n ≥ 0;
+    decreases n; */
+int __gen_e_acsl_odd(int n)
+{
+  int __retres;
+  __e_acsl_assert(n >= 0,1,"Precondition","odd","n >= 0",
+                  "tests/constructs/decrease.i",54);
+  __retres = odd(n);
+  return __retres;
+}
+
+/*@ decreases n; */
+int __gen_e_acsl_fib(int n)
+{
+  int __retres;
+  __retres = fib(n);
+  return __retres;
+}
+
+/*@ requires n ≤ 12; */
+int __gen_e_acsl_fact(int n)
+{
+  int __retres;
+  __e_acsl_assert(n <= 12,1,"Precondition","fact","n <= 12",
+                  "tests/constructs/decrease.i",26);
+  __retres = fact(n);
+  return __retres;
+}
+
+int __gen_e_acsl_lexico(int x, int y)
+{
+  int __gen_e_acsl_and;
+  if (x > y) __gen_e_acsl_and = 0 <= x; else __gen_e_acsl_and = 0;
+  return __gen_e_acsl_and;
+}
+
+

src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle

@@ -4,8 +4,6 @@
 [e-acsl] tests/special/e-acsl-valid.c:28: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:26: Warning: 
-  E-ACSL construct `variant' is not yet supported. Ignoring annotation.
 [e-acsl] tests/special/e-acsl-valid.c:24: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.

src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c

@@ -26,6 +26,7 @@ void __gen_e_acsl_f(int *x, int *y);
 
 void f(int *x, int *y)
 {
+  long __gen_e_acsl_old_variant;
   {
     int __gen_e_acsl_valid_read;
     __e_acsl_store_block((void *)(& y),(size_t)8);
@@ -51,10 +52,18 @@ void f(int *x, int *y)
     int i = 0;
     /*@ loop invariant 0 ≤ i ≤ 1;
         loop variant 2 - i; */
-    while (i < 1) {
+    while (1) {
+      __gen_e_acsl_old_variant = 2L - i;
+      if (! (i < 1)) break;
       /*@ assert 1 ≡ 1; */ ;
       /*@ assert \valid(y); */ ;
       i ++;
+      __e_acsl_assert(__gen_e_acsl_old_variant >= 0L,1,"Variant","f",
+                      "(old 2 - i) \342\211\245 0",
+                      "tests/special/e-acsl-valid.c",31);
+      __e_acsl_assert(__gen_e_acsl_old_variant > 2L - i,1,"Variant","f",
+                      "(old 2 - i) > 2 - i","tests/special/e-acsl-valid.c",
+                      31);
     }
   }
   __e_acsl_delete_block((void *)(& y));