diff --git a/src/plugins/e-acsl/tests/gmp/functions_rec.c b/src/plugins/e-acsl/tests/gmp/functions_rec.c
index 3619ab7c793d4083b6b843a7b02bd2eaa835c380..76c60912194b4481bc8e6f06bb94b8f522b6a2d4 100644
--- a/src/plugins/e-acsl/tests/gmp/functions_rec.c
+++ b/src/plugins/e-acsl/tests/gmp/functions_rec.c
@@ -1,5 +1,6 @@
/* run.config
COMMENT: recursive logic functions
+ STDOPT: +"-eva-ignore-recursive-calls"
*/
/*@ logic integer f1(integer n) =
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
index c7a7f721fbe4ce2b251aafc6e540ffadc82ee415..cbf74d13ac79e1568bba0f82bc91e82493871cf4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
@@ -10,78 +10,78 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/functions_rec.c:25:
+[eva] tests/gmp/functions_rec.c:26:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[eva:alarm] tests/gmp/functions_rec.c:25: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva] using specification for function __gen_e_acsl_f2_2
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow.
assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:25: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/functions_rec.c:27:
+[eva] tests/gmp/functions_rec.c:28:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
-[eva:alarm] tests/gmp/functions_rec.c:27: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:13: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:14: Warning:
recursive call during value analysis
- of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:13 <-
- __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:27 <-
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva] using specification for function __gen_e_acsl_f3_2
-[eva] tests/gmp/functions_rec.c:29:
+[eva] tests/gmp/functions_rec.c:30:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
-[eva:alarm] tests/gmp/functions_rec.c:29: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:16: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
+[eva] tests/gmp/functions_rec.c:17: Warning:
recursive call during value analysis
- of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:16 <-
- __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:29 <-
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
main).
Assuming the call has no effect. The analysis will be unsound.
[eva] using specification for function __gen_e_acsl_f4_2
-[eva:alarm] tests/gmp/functions_rec.c:29: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
index 723a7954d81f95b1f8de0ff2545b2d17ca1245ce..ad15ac476ccad3eb4c1c7c322456de28b5dc3c3f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
@@ -10,107 +10,107 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[eva] using specification for function __e_acsl_memory_init
-[eva] tests/gmp/functions_rec.c:25:
+[eva] tests/gmp/functions_rec.c:26:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[eva:alarm] tests/gmp/functions_rec.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_cmp
[eva] using specification for function __gmpz_init_set
[eva] using specification for function __gmpz_clear
[eva] using specification for function __gmpz_init
[eva] using specification for function __gmpz_sub
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
[eva] using specification for function __gen_e_acsl_f2_2
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
[eva] using specification for function __gmpz_mul
-[eva] tests/gmp/functions_rec.c:9: Warning:
+[eva] tests/gmp/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:9 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:25 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
[eva] :0:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f2
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
assertion 'E_ACSL' got status unknown.
[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpz_tdiv_q
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
-[eva:alarm] tests/gmp/functions_rec.c:9: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
-[eva:alarm] tests/gmp/functions_rec.c:25: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/functions_rec.c:27:
+[eva] tests/gmp/functions_rec.c:28:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f3
-[eva:alarm] tests/gmp/functions_rec.c:27: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:13: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
[eva] using specification for function __gmpz_get_si
-[eva] tests/gmp/functions_rec.c:13: Warning:
+[eva] tests/gmp/functions_rec.c:14: Warning:
recursive call during value analysis
- of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:13 <-
- __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:27 <-
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:13: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
[eva] using specification for function __gen_e_acsl_f3_2
[eva] using specification for function __gmpz_add
-[eva:alarm] tests/gmp/functions_rec.c:13: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
-[eva:alarm] tests/gmp/functions_rec.c:13: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:14: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
[eva] using specification for function __gmpz_neg
-[eva:alarm] tests/gmp/functions_rec.c:27: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:28: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva] tests/gmp/functions_rec.c:29:
+[eva] tests/gmp/functions_rec.c:30:
cannot evaluate ACSL term, unsupported ACSL construct: logic function f4
-[eva:alarm] tests/gmp/functions_rec.c:29: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:16: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/functions_rec.c:17: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
-[eva] tests/gmp/functions_rec.c:16: Warning:
+[eva] tests/gmp/functions_rec.c:17: Warning:
recursive call during value analysis
- of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:16 <-
- __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:29 <-
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:16: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:17: Warning:
accessing uninitialized left-value.
assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
[eva] using specification for function __gen_e_acsl_f4_2
[eva] using specification for function __gmpz_init_set_ui
-[eva:alarm] tests/gmp/functions_rec.c:29: Warning:
+[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
index 5c263c6479ea5fb876a26a785e731823d86d6680..0fa4a22a630c4d80f8f44b38a7c561a6b5e93f13 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
@@ -39,26 +39,60 @@ int main(void)
int __gen_e_acsl_f2_14;
__gen_e_acsl_f2_14 = __gen_e_acsl_f2(7);
__e_acsl_assert(__gen_e_acsl_f2_14 == 1,(char *)"Assertion",
- (char *)"main",(char *)"f2(7) == 1",25);
+ (char *)"main",(char *)"f2(7) == 1",26);
}
/*@ assert f3(6) ≡ -5; */
{
int __gen_e_acsl_f3_6;
__gen_e_acsl_f3_6 = __gen_e_acsl_f3(6);
__e_acsl_assert(__gen_e_acsl_f3_6 == -5,(char *)"Assertion",
- (char *)"main",(char *)"f3(6) == -5",27);
+ (char *)"main",(char *)"f3(6) == -5",28);
}
/*@ assert f4(9) > 0; */
{
unsigned long __gen_e_acsl_f4_6;
__gen_e_acsl_f4_6 = __gen_e_acsl_f4(9);
__e_acsl_assert(__gen_e_acsl_f4_6 > 0UL,(char *)"Assertion",
- (char *)"main",(char *)"f4(9) > 0",29);
+ (char *)"main",(char *)"f4(9) > 0",30);
}
__retres = 0;
return __retres;
}
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_6;
+ if (n < 100L) {
+ unsigned long __gen_e_acsl_f4_4;
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_5;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
+ else __gen_e_acsl_if_5 = 6UL;
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_8;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_5;
+ __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_5;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_7;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
int __gen_e_acsl_f2_2(long n)
{
int __gen_e_acsl_if;
@@ -71,7 +105,7 @@ int __gen_e_acsl_f2_2(long n)
__gen_e_acsl_f2_6 = __gen_e_acsl_f2_2(n - 2L);
__gen_e_acsl_f2_8 = __gen_e_acsl_f2_2(n - 3L);
__e_acsl_assert(__gen_e_acsl_f2_8 != 0,(char *)"RTE",(char *)"f2_2",
- (char *)"division_by_zero: __gen_e_acsl_f2_8 != 0",9);
+ (char *)"division_by_zero: __gen_e_acsl_f2_8 != 0",10);
/*@ assert Eva: division_by_zero: __gen_e_acsl_f2_8 ≢ 0; */
/*@ assert
Eva: signed_overflow:
@@ -103,7 +137,7 @@ int __gen_e_acsl_f2(int n)
__gen_e_acsl_f2_11 = __gen_e_acsl_f2_2(n - 2L);
__gen_e_acsl_f2_13 = __gen_e_acsl_f2_2(n - 3L);
__e_acsl_assert(__gen_e_acsl_f2_13 != 0,(char *)"RTE",(char *)"f2",
- (char *)"division_by_zero: __gen_e_acsl_f2_13 != 0",9);
+ (char *)"division_by_zero: __gen_e_acsl_f2_13 != 0",10);
/*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
/*@ assert
Eva: signed_overflow:
@@ -171,38 +205,4 @@ int __gen_e_acsl_f3(int n)
return __gen_e_acsl_if_4;
}
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_6;
- if (n < 100L) {
- unsigned long __gen_e_acsl_f4_4;
- __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_f4_4;
- }
- else {
- unsigned long __gen_e_acsl_if_5;
- if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
- else __gen_e_acsl_if_5 = 6UL;
- __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
- }
- return __gen_e_acsl_if_6;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_8;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_5;
- __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_8 = __gen_e_acsl_f4_5;
- }
- else {
- unsigned long __gen_e_acsl_if_7;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
- else __gen_e_acsl_if_7 = 6UL;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
- }
- return __gen_e_acsl_if_8;
-}
-
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
index b7ac1c6bd4b51843d645e4b1f469c5541232d848..c13d6d1e49b1ef2fae4f1c8c5fb0922a23127c3f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
@@ -47,7 +47,7 @@ int main(void)
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_14),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
- (char *)"f2(7) == 1",25);
+ (char *)"f2(7) == 1",26);
__gmpz_clear(__gen_e_acsl_f2_14);
__gmpz_clear(__gen_e_acsl__13);
}
@@ -65,7 +65,7 @@ int main(void)
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_neg));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
- (char *)"main",(char *)"f3(6) == -5",27);
+ (char *)"main",(char *)"f3(6) == -5",28);
__gmpz_clear(__gen_e_acsl_f3_6);
__gmpz_clear(__gen_e_acsl__23);
__gmpz_clear(__gen_e_acsl_neg);
@@ -80,7 +80,7 @@ int main(void)
__gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_6),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__34));
__e_acsl_assert(__gen_e_acsl_gt_3 > 0,(char *)"Assertion",(char *)"main",
- (char *)"f4(9) > 0",29);
+ (char *)"f4(9) > 0",30);
__gmpz_clear(__gen_e_acsl_f4_6);
__gmpz_clear(__gen_e_acsl__34);
}
@@ -88,6 +88,138 @@ int main(void)
return __retres;
}
+void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ int __gen_e_acsl_lt_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
+ __gmpz_init_set_si(__gen_e_acsl__26,100L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ if (__gen_e_acsl_lt_4 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__27;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl_f4_4;
+ __gmpz_init_set_si(__gen_e_acsl__27,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ */
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_4));
+ __gmpz_clear(__gen_e_acsl__27);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_f4_4);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__28;
+ int __gen_e_acsl_lt_5;
+ __e_acsl_mpz_t __gen_e_acsl_if_5;
+ __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
+ if (__gen_e_acsl_lt_5 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__29;
+ __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ __gmpz_clear(__gen_e_acsl__29);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__30;
+ __gmpz_init_set_si(__gen_e_acsl__30,6L);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
+ __gmpz_clear(__gen_e_acsl__30);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
+ __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_clear(__gen_e_acsl_if_5);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl__26);
+ __gmpz_clear(__gen_e_acsl_if_6);
+ return;
+}
+
+void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ int __gen_e_acsl_lt_3;
+ __e_acsl_mpz_t __gen_e_acsl_if_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__24,100L);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ if (__gen_e_acsl_lt_3 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl_n_7;
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_f4_5;
+ __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__25,1L);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ */
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
+ __gmpz_clear(__gen_e_acsl_n_7);
+ __gmpz_clear(__gen_e_acsl__25);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_f4_5);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl__31;
+ int __gen_e_acsl_lt_6;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
+ __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
+ __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ if (__gen_e_acsl_lt_6 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__32;
+ __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ __gmpz_clear(__gen_e_acsl__32);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__33;
+ __gmpz_init_set_si(__gen_e_acsl__33,6L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ __gmpz_clear(__gen_e_acsl__33);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl__31);
+ __gmpz_clear(__gen_e_acsl_if_7);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
+ __gmpz_clear(__gen_e_acsl_n_6);
+ __gmpz_clear(__gen_e_acsl__24);
+ __gmpz_clear(__gen_e_acsl_if_8);
+ return;
+}
+
void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
{
__e_acsl_mpz_t __gen_e_acsl__4;
@@ -157,7 +289,7 @@ void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: f2(n - 3) ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),(char *)"Assertion",
- (char *)"f2_2",(char *)"f2(n - 3) == 0",9);
+ (char *)"f2_2",(char *)"f2(n - 3) == 0",10);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8));
@@ -259,7 +391,7 @@ void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: f2(n - 3) ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
- (char *)"f2",(char *)"f2(n - 3) == 0",9);
+ (char *)"f2",(char *)"f2(n - 3) == 0",10);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13));
@@ -458,136 +590,4 @@ void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n)
return;
}
-void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__26;
- int __gen_e_acsl_lt_4;
- __e_acsl_mpz_t __gen_e_acsl_if_6;
- __gmpz_init_set_si(__gen_e_acsl__26,100L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- if (__gen_e_acsl_lt_4 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__27;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __e_acsl_mpz_t __gen_e_acsl_f4_4;
- __gmpz_init_set_si(__gen_e_acsl__27,1L);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- */
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_4));
- __gmpz_clear(__gen_e_acsl__27);
- __gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl_f4_4);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__28;
- int __gen_e_acsl_lt_5;
- __e_acsl_mpz_t __gen_e_acsl_if_5;
- __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- if (__gen_e_acsl_lt_5 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__29;
- __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_clear(__gen_e_acsl__29);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__30;
- __gmpz_init_set_si(__gen_e_acsl__30,6L);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
- __gmpz_clear(__gen_e_acsl__30);
- }
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
- __gmpz_clear(__gen_e_acsl__28);
- __gmpz_clear(__gen_e_acsl_if_5);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
- __gmpz_clear(__gen_e_acsl__26);
- __gmpz_clear(__gen_e_acsl_if_6);
- return;
-}
-
-void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_n_6;
- __e_acsl_mpz_t __gen_e_acsl__24;
- int __gen_e_acsl_lt_3;
- __e_acsl_mpz_t __gen_e_acsl_if_8;
- __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__24,100L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- if (__gen_e_acsl_lt_3 < 0) {
- __e_acsl_mpz_t __gen_e_acsl_n_7;
- __e_acsl_mpz_t __gen_e_acsl__25;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl_f4_5;
- __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__25,1L);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
- */
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
- __gmpz_clear(__gen_e_acsl_n_7);
- __gmpz_clear(__gen_e_acsl__25);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl_f4_5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_8;
- __e_acsl_mpz_t __gen_e_acsl__31;
- int __gen_e_acsl_lt_6;
- __e_acsl_mpz_t __gen_e_acsl_if_7;
- __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
- __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
- __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- if (__gen_e_acsl_lt_6 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__32;
- __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
- __gmpz_clear(__gen_e_acsl__32);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__33;
- __gmpz_init_set_si(__gen_e_acsl__33,6L);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
- __gmpz_clear(__gen_e_acsl__33);
- }
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl__31);
- __gmpz_clear(__gen_e_acsl_if_7);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
- __gmpz_clear(__gen_e_acsl_n_6);
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_if_8);
- return;
-}
-