Commit 6eb942ce authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] add -eva-ignore-recursive-calls when testing recursive logic functions...

[tests] add -eva-ignore-recursive-calls when testing recursive logic functions (unfortunately removed when the branch was rebased)
parent 0f8749e2
/* run.config
COMMENT: recursive logic functions
STDOPT: +"-eva-ignore-recursive-calls"
*/
/*@ logic integer f1(integer n) =
......
......@@ -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
......@@ -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
......@@ -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;
}
......@@ -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 {