diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index f2937821bc68e16241c86164a9964f1a9e12c215..125ffabd7c5e84213944bece0b0ba2250cb4a0b1 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -377,7 +377,6 @@ let rec fixpoint ~(infer : force:bool ->
let assumed_ival = interv_of_typ_containing_interv inferred_ival in
fixpoint ~infer li args_ival t' assumed_ival
-
(* Memoization module which retrieves the computed info of some terms *)
module Memo: sig
val memo:
@@ -482,8 +481,6 @@ end = struct
let clear () =
Options.feedback ~level:4 "clearing the typing tables";
LFProf.Hashtbl.clear widened_profile_tbl
-
-
end
let plus_one i =
@@ -742,17 +739,18 @@ let rec infer ~force ~logic_env t =
if LF_env.is_rec li then
let widened_profile = widen_profile profile in
Widened_profile.add profile li widened_profile;
- (match li.l_body with
- | LBpred p ->
- LF_env.add_pred li widened_profile;
- infer_predicate
- ~logic_env:(Logic_env.make widened_profile) p;
- Ival Ival.zero_or_one
- | LBterm t' ->
- (try LF_env.find li widened_profile
- with Not_found ->
- fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
- | _ -> assert false)
+ try LF_env.find li widened_profile
+ with
+ | Not_found ->
+ (match li.l_body with
+ | LBpred p ->
+ LF_env.add_pred li widened_profile;
+ infer_predicate
+ ~logic_env:(Logic_env.make widened_profile) p;
+ Ival Ival.zero_or_one
+ | LBterm t' ->
+ fixpoint ~infer li widened_profile t' (Ival Ival.bottom)
+ | _ -> assert false)
else
let logic_env = Logic_env.make profile in
(match li.l_body with
@@ -1059,8 +1057,11 @@ and infer_predicate ~logic_env p =
infer_predicate ~logic_env p;
| Pif(t, p1, p2) ->
ignore (infer ~force:false ~logic_env t);
- infer_predicate ~logic_env p1;
- infer_predicate ~logic_env p2
+ let logic_env_tbranch, logic_env_fbranch =
+ compute_logic_env_if_branches logic_env t
+ in
+ infer_predicate ~logic_env:logic_env_tbranch p1;
+ infer_predicate ~logic_env:logic_env_fbranch p2
| Plet(li, p) ->
let li_t = Misc.term_of_li li in
let li_v = li.l_var_info in
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index 6332bd48d4b8d961b978cbf1ee83e7f3f568e931..f53305dc5bcad0814d39ca78341b1a0304480a20 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -1,28 +1,16 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions_rec.c:11: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
-[eva:alarm] functions_rec.c:11: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
[eva] functions_rec.c:11: Warning:
- Using specification of function __gen_e_acsl_even_3 for recursive calls.
- Analysis of function __gen_e_acsl_even_3 is thus incomplete and its soundness
- relies on the written specification.
-[eva:alarm] functions_rec.c:12: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
-[eva] functions_rec.c:12: Warning:
- Using specification of function __gen_e_acsl_even_3 for recursive calls.
- Analysis of function __gen_e_acsl_even_3 is thus incomplete and its soundness
+ Using specification of function __gen_e_acsl_even for recursive calls.
+ Analysis of function __gen_e_acsl_even is thus incomplete and its soundness
relies on the written specification.
[eva:alarm] functions_rec.c:40: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:40: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:12: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+[eva] functions_rec.c:12: Warning:
+ Using specification of function __gen_e_acsl_even for recursive calls.
+ Analysis of function __gen_e_acsl_even is thus incomplete and its soundness
+ relies on the written specification.
[eva:alarm] functions_rec.c:41: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:41: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index 7c2bcabacd397e0c75e4c589de4872c23e20b9ff..7d95aadc010abf548b870ae7719e59590b93dfc6 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -11,14 +11,9 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
/*@
predicate even(integer n) =
n == 0? \true: (n > 0? !even(n - 1): !even(n + 1));
-
-*/
-int __gen_e_acsl_even_2(long n);
-
+ */
int __gen_e_acsl_even(int n);
-int __gen_e_acsl_even_3(__e_acsl_mpz_struct * n);
-
/*@
predicate even_and_not_negative(integer n) =
n == 0? \true: (n > 0? !even(n - 1): \false);
@@ -62,35 +57,35 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
{
- int __gen_e_acsl_even_14;
+ int __gen_e_acsl_even_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_even_14 = __gen_e_acsl_even(10);
+ __gen_e_acsl_even_6 = __gen_e_acsl_even(10);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"even(10)",0,
- __gen_e_acsl_even_14);
+ __gen_e_acsl_even_6);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
__gen_e_acsl_assert_data.pred_txt = "even(10)";
__gen_e_acsl_assert_data.file = "functions_rec.c";
__gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 40;
- __e_acsl_assert(__gen_e_acsl_even_14,& __gen_e_acsl_assert_data);
+ __e_acsl_assert(__gen_e_acsl_even_6,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
/*@ assert even(10); */ ;
{
- int __gen_e_acsl_even_16;
+ int __gen_e_acsl_even_8;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_even_16 = __gen_e_acsl_even(-6);
+ __gen_e_acsl_even_8 = __gen_e_acsl_even(-6);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"even(-6)",0,
- __gen_e_acsl_even_16);
+ __gen_e_acsl_even_8);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "even(-6)";
__gen_e_acsl_assert_data_2.file = "functions_rec.c";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 41;
- __e_acsl_assert(__gen_e_acsl_even_16,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_even_8,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
/*@ assert even(-6); */ ;
@@ -116,14 +111,14 @@ int main(void)
/*@ assert even_and_not_negative(10); */ ;
{
__e_acsl_mpz_t __gen_e_acsl_f1_4;
- __e_acsl_mpz_t __gen_e_acsl__8;
- int __gen_e_acsl_eq_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_eq;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
__gen_e_acsl_f1(& __gen_e_acsl_f1_4,0);
- __gmpz_init_set_si(__gen_e_acsl__8,0L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_4,"f1(0)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4));
__gen_e_acsl_assert_data_4.blocking = 1;
@@ -132,22 +127,22 @@ int main(void)
__gen_e_acsl_assert_data_4.file = "functions_rec.c";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 43;
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__gmpz_clear(__gen_e_acsl_f1_4);
- __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl__2);
}
/*@ assert f1(0) == 0; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl__9;
- int __gen_e_acsl_eq_3;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
__gen_e_acsl_f1(& __gen_e_acsl_f1_6,1);
- __gmpz_init_set_si(__gen_e_acsl__9,1L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_5,"f1(1)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
__gen_e_acsl_assert_data_5.blocking = 1;
@@ -156,22 +151,22 @@ int main(void)
__gen_e_acsl_assert_data_5.file = "functions_rec.c";
__gen_e_acsl_assert_data_5.fct = "main";
__gen_e_acsl_assert_data_5.line = 44;
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
__gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__3);
}
/*@ assert f1(1) == 1; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__10;
- int __gen_e_acsl_eq_4;
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ int __gen_e_acsl_eq_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
{.values = (void *)0};
__gen_e_acsl_f1(& __gen_e_acsl_f1_8,10);
- __gmpz_init_set_si(__gen_e_acsl__10,55L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_init_set_si(__gen_e_acsl__4,55L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"f1(10)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8));
__gen_e_acsl_assert_data_6.blocking = 1;
@@ -180,22 +175,22 @@ int main(void)
__gen_e_acsl_assert_data_6.file = "functions_rec.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 45;
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__4);
}
/*@ assert f1(10) == 55; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_f2_8;
- __e_acsl_mpz_t __gen_e_acsl__13;
- int __gen_e_acsl_eq_5;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
{.values = (void *)0};
__gen_e_acsl_f2(& __gen_e_acsl_f2_8,7);
- __gmpz_init_set_si(__gen_e_acsl__13,1L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
/*@ assert Eva: initialization: \initialized(&n); */
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,"n",0,n);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_8,"f2(n - 3)",0,
@@ -208,10 +203,10 @@ int main(void)
__gen_e_acsl_assert_data_7.file = "functions_rec.c";
__gen_e_acsl_assert_data_7.fct = "main";
__gen_e_acsl_assert_data_7.line = 47;
- __e_acsl_assert(__gen_e_acsl_eq_5 == 0,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gmpz_clear(__gen_e_acsl_f2_8);
- __gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl__7);
}
/*@ assert f2(7) == 1; */ ;
{
@@ -250,14 +245,14 @@ int main(void)
/*@ assert f4(9) > 0; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_f5_4;
- __e_acsl_mpz_t __gen_e_acsl__15;
- int __gen_e_acsl_eq_6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__gen_e_acsl_f5(& __gen_e_acsl_f5_4,0);
- __gmpz_init_set_si(__gen_e_acsl__15,0L);
- __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_11,"f5(0)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4));
__gen_e_acsl_assert_data_11.blocking = 1;
@@ -266,26 +261,26 @@ int main(void)
__gen_e_acsl_assert_data_11.file = "functions_rec.c";
__gen_e_acsl_assert_data_11.fct = "main";
__gen_e_acsl_assert_data_11.line = 53;
- __e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_11);
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
__gmpz_clear(__gen_e_acsl_f5_4);
- __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl__9);
}
/*@ assert f5(0) == 0; */ ;
{
- long __gen_e_acsl_n_5;
+ long __gen_e_acsl_n_3;
__e_acsl_mpz_t __gen_e_acsl_f5_8;
- __e_acsl_mpz_t __gen_e_acsl__17;
- int __gen_e_acsl_eq_7;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
- __gen_e_acsl_n_5 = 9223372036854775807L;
- __gen_e_acsl_f5_5(& __gen_e_acsl_f5_8,__gen_e_acsl_n_5);
- __gmpz_init_set_si(__gen_e_acsl__17,0L);
- __gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __gen_e_acsl_n_3 = 9223372036854775807L;
+ __gen_e_acsl_f5_5(& __gen_e_acsl_f5_8,__gen_e_acsl_n_3);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert_register_long(& __gen_e_acsl_assert_data_12,"n",0,
- __gen_e_acsl_n_5);
+ __gen_e_acsl_n_3);
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_12,"f5(n)",0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8));
__gen_e_acsl_assert_data_12.blocking = 1;
@@ -294,10 +289,10 @@ int main(void)
__gen_e_acsl_assert_data_12.file = "functions_rec.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 55;
- __e_acsl_assert(__gen_e_acsl_eq_7 == 0,& __gen_e_acsl_assert_data_12);
+ __e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
__gmpz_clear(__gen_e_acsl_f5_8);
- __gmpz_clear(__gen_e_acsl__17);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert \let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0; */ ;
__retres = 0;
@@ -305,140 +300,26 @@ int main(void)
return __retres;
}
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_even_2(long n)
-{
- int __gen_e_acsl_if_4;
- if (n == 0L) __gen_e_acsl_if_4 = 1;
- else {
- int __gen_e_acsl_if_3;
- if (n > 0L) {
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- int __gen_e_acsl_even_8;
- __gmpz_init_set_si(__gen_e_acsl_n,n);
- __gmpz_init_set_si(__gen_e_acsl_,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- */
- __gen_e_acsl_even_8 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- __gen_e_acsl_if_3 = ! __gen_e_acsl_even_8;
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_sub);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl__6;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- int __gen_e_acsl_even_10;
- __gmpz_init_set_si(__gen_e_acsl_n_2,n);
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
- */
- __gen_e_acsl_even_10 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
- __gen_e_acsl_if_3 = ! __gen_e_acsl_even_10;
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_add_2);
- }
- __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
- }
- return __gen_e_acsl_if_4;
-}
-
/*@ assigns \result;
assigns \result \from n; */
int __gen_e_acsl_even(int n)
{
- int __gen_e_acsl_if_6;
- if (n == 0) __gen_e_acsl_if_6 = 1;
+ int __gen_e_acsl_if_2;
+ if (n == 0) __gen_e_acsl_if_2 = 1;
else {
- int __gen_e_acsl_if_5;
+ int __gen_e_acsl_if;
if (n > 0) {
- int __gen_e_acsl_even_11;
- __gen_e_acsl_even_11 = __gen_e_acsl_even_2(n - 1L);
- __gen_e_acsl_if_5 = ! __gen_e_acsl_even_11;
+ int __gen_e_acsl_even_3;
+ __gen_e_acsl_even_3 = __gen_e_acsl_even(n - 1);
+ __gen_e_acsl_if = ! __gen_e_acsl_even_3;
}
else {
- int __gen_e_acsl_even_13;
- __gen_e_acsl_even_13 = __gen_e_acsl_even_2(n + 1L);
- __gen_e_acsl_if_5 = ! __gen_e_acsl_even_13;
- }
- __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
- }
- return __gen_e_acsl_if_6;
-}
-
-/*@ assigns \result;
- assigns \result \from *((__e_acsl_mpz_struct *)n); */
-int __gen_e_acsl_even_3(__e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq;
- int __gen_e_acsl_if_2;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- if (__gen_e_acsl_eq == 0) __gen_e_acsl_if_2 = 1;
- else {
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_gt;
- int __gen_e_acsl_if;
- __gmpz_init_set_si(__gen_e_acsl__3,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- if (__gen_e_acsl_gt > 0) {
- __e_acsl_mpz_t __gen_e_acsl__4;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
int __gen_e_acsl_even_5;
- __gmpz_init_set_si(__gen_e_acsl__4,1L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
- */
- __gen_e_acsl_even_5 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gen_e_acsl_even_5 = __gen_e_acsl_even(n + 1);
__gen_e_acsl_if = ! __gen_e_acsl_even_5;
- __gmpz_clear(__gen_e_acsl__4);
- __gmpz_clear(__gen_e_acsl_sub_2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __e_acsl_mpz_t __gen_e_acsl_add;
- int __gen_e_acsl_even_7;
- __gmpz_init_set_si(__gen_e_acsl__5,1L);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
- */
- __gen_e_acsl_even_7 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_add);
- __gen_e_acsl_if = ! __gen_e_acsl_even_7;
- __gmpz_clear(__gen_e_acsl__5);
- __gmpz_clear(__gen_e_acsl_add);
}
__gen_e_acsl_if_2 = __gen_e_acsl_if;
- __gmpz_clear(__gen_e_acsl__3);
}
- __gmpz_clear(__gen_e_acsl__2);
return __gen_e_acsl_if_2;
}
@@ -446,52 +327,52 @@ int __gen_e_acsl_even_3(__e_acsl_mpz_struct * n)
assigns \result \from n; */
int __gen_e_acsl_even_and_not_negative(int n)
{
- int __gen_e_acsl_if_8;
- if (n == 0) __gen_e_acsl_if_8 = 1;
+ int __gen_e_acsl_if_4;
+ if (n == 0) __gen_e_acsl_if_4 = 1;
else {
- int __gen_e_acsl_if_7;
+ int __gen_e_acsl_if_3;
if (n > 0) {
- int __gen_e_acsl_even_18;
- __gen_e_acsl_even_18 = __gen_e_acsl_even(n - 1);
- __gen_e_acsl_if_7 = ! __gen_e_acsl_even_18;
+ int __gen_e_acsl_even_10;
+ __gen_e_acsl_even_10 = __gen_e_acsl_even(n - 1);
+ __gen_e_acsl_if_3 = ! __gen_e_acsl_even_10;
}
- else __gen_e_acsl_if_7 = 0;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ else __gen_e_acsl_if_3 = 0;
+ __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
}
- return __gen_e_acsl_if_8;
+ return __gen_e_acsl_if_4;
}
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_9;
+ __e_acsl_mpz_t __gen_e_acsl_if_5;
if (n <= 0) {
- __e_acsl_mpz_t __gen_e_acsl__7;
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
- __gmpz_init_set(__gen_e_acsl_if_9,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
- __gmpz_clear(__gen_e_acsl__7);
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
}
else {
__e_acsl_mpz_t __gen_e_acsl_f1_3;
- __e_acsl_mpz_t __gen_e_acsl_n_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_add;
__gen_e_acsl_f1(& __gen_e_acsl_f1_3,n - 1);
- __gmpz_init_set_si(__gen_e_acsl_n_3,(long)n);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
- __gmpz_init_set(__gen_e_acsl_if_9,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
__gmpz_clear(__gen_e_acsl_f1_3);
- __gmpz_clear(__gen_e_acsl_n_3);
- __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_add);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_9));
- __gmpz_clear(__gen_e_acsl_if_9);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
+ __gmpz_clear(__gen_e_acsl_if_5);
return;
}
@@ -499,20 +380,20 @@ void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_10;
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
if (n < 0) {
- __e_acsl_mpz_t __gen_e_acsl__11;
- __gmpz_init_set_si(__gen_e_acsl__11,1L);
- __gmpz_init_set(__gen_e_acsl_if_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_clear(__gen_e_acsl__11);
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_clear(__gen_e_acsl__5);
}
else {
__e_acsl_mpz_t __gen_e_acsl_f2_3;
__e_acsl_mpz_t __gen_e_acsl_f2_5;
__e_acsl_mpz_t __gen_e_acsl_mul;
__e_acsl_mpz_t __gen_e_acsl_f2_7;
- __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl__6;
int __gen_e_acsl_div_guard;
__e_acsl_mpz_t __gen_e_acsl_div;
__gen_e_acsl_f2(& __gen_e_acsl_f2_3,n - 1);
@@ -524,9 +405,9 @@ void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
__gen_e_acsl_f2(& __gen_e_acsl_f2_7,n - 3);
- __gmpz_init_set_si(__gen_e_acsl__12,0L);
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
__gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: f2(n - 3) != 0; */
{
@@ -543,18 +424,18 @@ void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
__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_7));
- __gmpz_init_set(__gen_e_acsl_if_10,
+ __gmpz_init_set(__gen_e_acsl_if_6,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
__gmpz_clear(__gen_e_acsl_f2_3);
__gmpz_clear(__gen_e_acsl_f2_5);
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl_f2_7);
- __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_div);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_10));
- __gmpz_clear(__gen_e_acsl_if_10);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl_if_6);
return;
}
@@ -578,72 +459,72 @@ int __gen_e_acsl_g(unsigned int n)
assigns \result \from n; */
int __gen_e_acsl_f3(int n)
{
- int __gen_e_acsl_if_11;
+ int __gen_e_acsl_if_7;
if (n > 0) {
int __gen_e_acsl_g_2;
int __gen_e_acsl_f3_3;
__gen_e_acsl_g_2 = __gen_e_acsl_g((unsigned int)n);
__gen_e_acsl_f3_3 = __gen_e_acsl_f3(n - 1);
- __gen_e_acsl_if_11 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_3 - 5;
+ __gen_e_acsl_if_7 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_3 - 5;
}
else {
int __gen_e_acsl_g_4;
__gen_e_acsl_g_4 = __gen_e_acsl_g_3(n + 1);
- __gen_e_acsl_if_11 = __gen_e_acsl_g_4;
+ __gen_e_acsl_if_7 = __gen_e_acsl_g_4;
}
- return __gen_e_acsl_if_11;
+ return __gen_e_acsl_if_7;
}
/*@ assigns \result;
assigns \result \from n; */
unsigned long __gen_e_acsl_f4(int n)
{
- unsigned long __gen_e_acsl_if_13;
+ unsigned long __gen_e_acsl_if_9;
if (n < 100) {
unsigned long __gen_e_acsl_f4_3;
__gen_e_acsl_f4_3 = __gen_e_acsl_f4(n + 1);
- __gen_e_acsl_if_13 = __gen_e_acsl_f4_3;
+ __gen_e_acsl_if_9 = __gen_e_acsl_f4_3;
}
else {
- unsigned long __gen_e_acsl_if_12;
- if ((unsigned long)n < 9223372036854775807UL) __gen_e_acsl_if_12 = 9223372036854775807UL;
- else __gen_e_acsl_if_12 = 6UL;
- __gen_e_acsl_if_13 = __gen_e_acsl_if_12;
+ unsigned long __gen_e_acsl_if_8;
+ if ((unsigned long)n < 9223372036854775807UL) __gen_e_acsl_if_8 = 9223372036854775807UL;
+ else __gen_e_acsl_if_8 = 6UL;
+ __gen_e_acsl_if_9 = __gen_e_acsl_if_8;
}
- return __gen_e_acsl_if_13;
+ return __gen_e_acsl_if_9;
}
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5_5(__e_acsl_mpz_t *__retres_arg, long n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_15;
+ __e_acsl_mpz_t __gen_e_acsl_if_11;
if (n >= 0L) {
- __e_acsl_mpz_t __gen_e_acsl__16;
- __gmpz_init_set_si(__gen_e_acsl__16,0L);
- __gmpz_init_set(__gen_e_acsl_if_15,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- __gmpz_clear(__gen_e_acsl__16);
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __gmpz_init_set_si(__gen_e_acsl__10,0L);
+ __gmpz_init_set(__gen_e_acsl_if_11,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_clear(__gen_e_acsl__10);
}
else {
__e_acsl_mpz_t __gen_e_acsl_f5_7;
- __e_acsl_mpz_t __gen_e_acsl_n_6;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
__gen_e_acsl_f5_5(& __gen_e_acsl_f5_7,n + 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_6,n);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
+ __gmpz_init_set_si(__gen_e_acsl_n_4,n);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6));
- __gmpz_init_set(__gen_e_acsl_if_15,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+ __gmpz_init_set(__gen_e_acsl_if_11,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
__gmpz_clear(__gen_e_acsl_f5_7);
- __gmpz_clear(__gen_e_acsl_n_6);
- __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl_add_3);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_15));
- __gmpz_clear(__gen_e_acsl_if_15);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_11));
+ __gmpz_clear(__gen_e_acsl_if_11);
return;
}
@@ -651,33 +532,33 @@ void __gen_e_acsl_f5_5(__e_acsl_mpz_t *__retres_arg, long n)
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_14;
+ __e_acsl_mpz_t __gen_e_acsl_if_10;
if (n >= 0) {
- __e_acsl_mpz_t __gen_e_acsl__14;
- __gmpz_init_set_si(__gen_e_acsl__14,0L);
- __gmpz_init_set(__gen_e_acsl_if_14,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- __gmpz_clear(__gen_e_acsl__14);
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init_set(__gen_e_acsl_if_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_clear(__gen_e_acsl__8);
}
else {
__e_acsl_mpz_t __gen_e_acsl_f5_3;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
__gen_e_acsl_f5(& __gen_e_acsl_f5_3,n + 1);
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
- __gmpz_init_set(__gen_e_acsl_if_14,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
__gmpz_clear(__gen_e_acsl_f5_3);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_14));
- __gmpz_clear(__gen_e_acsl_if_14);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_10));
+ __gmpz_clear(__gen_e_acsl_if_10);
return;
}