diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i
new file mode 100644
index 0000000000000000000000000000000000000000..b5dc3a50ca7515eb3f4fa32bcff259c351083bce
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/decrease.i
@@ -0,0 +1,87 @@
+/* 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;
+}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..74f4f63423966d0396e43ebbb9a02c8887c3ddcf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle
@@ -0,0 +1,73 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
new file mode 100644
index 0000000000000000000000000000000000000000..41a66ca7b5efb2a1f491aca7a9eefbe396862a59
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c
@@ -0,0 +1,226 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/decrease.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/decrease.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
index 2a20efd543f570f710b1f32d7177806c057ed931..6420addb008c45e48b24143a2062ccc305fbe9b7 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
index 5653d657ff06a0a63975ad0803668d46a9f06e70..8fd9ca39e0bf76b673897322fa3d71b82bcf9f84 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
+++ b/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));